Documentation

Actus.Contract.Agree

source
theorem Actus.Contract.Agree.pam_step_to_fun {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : s ↝[ct, rf] s') :
∃ (e : Protocol.EventType) (t : Protocol.Time), s' = PAM.stf ct rf e t s
source
theorem Actus.Contract.Agree.pam_fun_to_step {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} (ht : s.sd ≤ t) :
Nonempty (s ↝[ct, rf] PAM.stf_IP ct rf t s)

Completeness for the events that have a dedicated PAM constructor. (The dispatcher's catch-all events — PD, STD, XD, DV — are not part of the PAM schedule and have no constructor.)

source
theorem Actus.Contract.Agree.lam_step_to_fun {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : LAM.Step ct rf s s') :
∃ (e : Protocol.EventType) (t : Protocol.Time), s' = LAM.stf ct rf e t s
source
def Actus.Contract.Agree.lam_fun_to_step {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) {t : Protocol.Time} (ht : s.sd ≤ t) :
LAM.Step ct rf s (LAM.stf ct rf e t s)
Equations
Instances For
    source
    theorem Actus.Contract.Agree.nam_step_to_fun {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : NAM.Step ct rf s s') :
    ∃ (e : Protocol.EventType) (t : Protocol.Time), s' = NAM.stf ct rf e t s
    source
    def Actus.Contract.Agree.nam_fun_to_step {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) {t : Protocol.Time} (ht : s.sd ≤ t) :
    NAM.Step ct rf s (NAM.stf ct rf e t s)
    Equations
    Instances For
      source
      theorem Actus.Contract.Agree.ann_step_to_fun {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : ANN.Step ct rf s s') :
      ∃ (e : Protocol.EventType) (t : Protocol.Time), s' = ANN.stf ct rf e t s
      source
      def Actus.Contract.Agree.ann_fun_to_step {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) {t : Protocol.Time} (ht : s.sd ≤ t) :
      ANN.Step ct rf s (ANN.stf ct rf e t s)
      Equations
      Instances For
        source
        theorem Actus.Contract.Agree.ump_step_to_fun {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : UMP.Step ct rf s s') :
        ∃ (e : Protocol.EventType) (t : Protocol.Time), s' = UMP.stf ct rf e t s
        source
        def Actus.Contract.Agree.ump_fun_to_step {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) {t : Protocol.Time} (ht : s.sd ≤ t) :
        UMP.Step ct rf s (UMP.stf ct rf e t s)
        Equations
        Instances For
          source
          theorem Actus.Contract.Agree.swppv_step_to_fun {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : SWPPV.Step ct rf s s') :
          ∃ (e : Protocol.EventType) (t : Protocol.Time), s' = SWPPV.stf ct rf e t s
          source
          def Actus.Contract.Agree.swppv_fun_to_step {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) (t : Protocol.Time) (ht : s.sd ≤ t) :
          SWPPV.Step ct rf s (SWPPV.stf ct rf e t s)
          Equations
          Instances For
            source
            theorem Actus.Contract.Agree.lax_step_to_fun {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : LAX.Step ct rf s s') :
            ∃ (e : Protocol.EventType) (x : α) (t : Protocol.Time), s' = LAX.stf ct rf e x t s
            source
            def Actus.Contract.Agree.lax_fun_to_step {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) (x : α) {t : Protocol.Time} (ht : s.sd ≤ t) :
            LAX.Step ct rf s (LAX.stf ct rf e x t s)
            Equations
            Instances For