def Test.LAM.lam : Actus.Contract.Terms Float

Equations

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

theorem Test.LAM.pr_reduces_notional (rf : Actus.Contract.RiskFactorEnv Float) (t : Actus.Protocol.Time) (s : Actus.Contract.State Float) : (Actus.Contract.LAM.stf_PR lam rf t s).nt = s.nt - Actus.Contract.LAM.redeemed s.nt s.prnxt

A principal-redemption step reduces the notional by the redeemed amount (the instalment capped at the remaining notional).