def Actus.Contract.NAM.stf_PR {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) (t : Protocol.Time) (s : State α) : State α

Negative-amortizer principal redemption: the instalment covers accrued interest first; the remainder Prnxt − Ipac_{t+} reduces Nt.

Equations

• One or more equations did not get rendered due to their size.

def Actus.Contract.NAM.pof_PR {α : Type} [Amount α] [DecidableLE α] (rf : RiskFactorEnv α) (t : Protocol.Time) (s : State α) : α

Equations

• Actus.Contract.NAM.pof_PR rf t s = rf.curs t * s.nsc * Actus.Contract.LAM.redeemed s.nt (s.prnxt - s.ipac - rf.yf s.sd t * s.ipnr * s.ipcb)

def Actus.Contract.NAM.stf {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) (ev : Protocol.EventType) (t : Protocol.Time) (s : State α) : State α

Equations

• Actus.Contract.NAM.stf ct rf Actus.Protocol.EventType.PR t s = Actus.Contract.NAM.stf_PR ct rf t s
• Actus.Contract.NAM.stf ct rf ev t s = Actus.Contract.LAM.stf ct rf ev t s

def Actus.Contract.NAM.pof {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) (ev : Protocol.EventType) (t : Protocol.Time) (s : State α) : α

Equations

• Actus.Contract.NAM.pof ct rf Actus.Protocol.EventType.PR t s = Actus.Contract.NAM.pof_PR rf t s
• Actus.Contract.NAM.pof ct rf ev t s = Actus.Contract.LAM.pof ct rf ev t s

def Actus.Contract.NAM.init {α : Type} [Amount α] (ct : Terms α) (md t₀ : Protocol.Time) : State α

Initial state: as LAM but Prnxt = R(CNTRL)·PRNXT (§7.4).

Equations

• One or more equations did not get rendered due to their size.

inductive Actus.Contract.NAM.Step {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) : State α → State α → Type

• ev {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) {t : Protocol.Time} : s.sd ≤ t → Step ct rf s (stf ct rf e t s)

@[reducible, inline]

abbrev Actus.Contract.NAM.Trace {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) : State α → State α → Type

Equations

• Actus.Contract.NAM.Trace ct rf = Actus.Closures.Star (Actus.Contract.NAM.Step ct rf)

def Actus.Contract.NAM.getCashflow {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) {s s' : State α} (h : Step ct rf s s') : Protocol.Event × α

Equations

• Actus.Contract.NAM.getCashflow ct rf (Actus.Contract.NAM.Step.ev e a) = (((Actus.Contract.NAM.stf ct rf e t s).sd, e), Actus.Contract.NAM.pof ct rf e (Actus.Contract.NAM.stf ct rf e t s).sd s)

def Actus.Contract.NAM.getCashflows {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) {s s' : State α} : Trace ct rf s s' → List (Protocol.Event × α)

Equations

• Actus.Contract.NAM.getCashflows ct rf Actus.Closures.Star.refl = []
• Actus.Contract.NAM.getCashflows ct rf (Actus.Closures.Star.step h rest) = Actus.Contract.NAM.getCashflow ct rf h :: Actus.Contract.NAM.getCashflows ct rf rest

def Actus.Contract.NAM.NAM_contract : Abstract.ActusContract

Equations

• Actus.Contract.NAM.NAM_contract = { Terms := Actus.Contract.Terms Float, State := Actus.Contract.State Float }

def Actus.Contract.NAM.NAM_impl (ct : Terms Float) (rf : RiskFactorEnv Float) (s₀ : State Float) : Abstract.StateTransition NAM_contract

Equations

• One or more equations did not get rendered due to their size.