def Test.PAM.pam : Actus.Contract.Terms Float

Equations

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

def Test.PAM.rf : Actus.Contract.RiskFactorEnv Float

Equations

• Test.PAM.rf = Actus.Contract.RiskFactorEnv.id

def Test.PAM.s0 : Actus.Contract.State Float

Initial state (maturity at time 10, status date 0).

Equations

• Test.PAM.s0 = Actus.Contract.PAM.init Test.PAM.pam 10 0

def Test.PAM.s1 : Actus.Contract.State Float

After the Initial Exchange at time 1.

Equations

• Test.PAM.s1 = Actus.Contract.PAM.stf_IED Test.PAM.pam 1 Test.PAM.s0

def Test.PAM.s2 : Actus.Contract.State Float

After Maturity at time 2.

Equations

• Test.PAM.s2 = Actus.Contract.PAM.stf_MD 2 Test.PAM.s1

def Test.PAM.step₁ : s0 ↝[pam, rf] s1

Equations

• Test.PAM.step₁ = Actus.Contract.PAM.Step.ied Test.PAM.step₁._proof_1

def Test.PAM.step₂ : s1 ↝[pam, rf] s2

Equations

• Test.PAM.step₂ = Actus.Contract.PAM.Step.md Test.PAM.step₂._proof_1

def Test.PAM.trace : Actus.Contract.PAM.Trace pam rf s0 s2

Full trace s0 ↠ s2.

Equations

• Test.PAM.trace = Actus.Closures.Star.step Test.PAM.step₁ (Actus.Closures.Star.step Test.PAM.step₂ Actus.Closures.Star.refl)

theorem Test.PAM.cf_ied : Actus.Contract.PAM.getCashflow pam rf step₁ = ((1, Actus.Protocol.EventType.IED), Actus.Contract.PAM.pof_IED pam rf 1)

The IED cashflow carries the IED payoff at time 1.

theorem Test.PAM.cf_md : Actus.Contract.PAM.getCashflow pam rf step₂ = ((2, Actus.Protocol.EventType.MD), Actus.Contract.PAM.pof_MD rf 2 s1)

The MD cashflow carries the redemption payoff at time 2.

def Test.PAM.cashflows : Actus.Protocol.Cashflows

Equations

• Test.PAM.cashflows = Actus.Contract.PAM.getCashflows Test.PAM.pam Test.PAM.rf Test.PAM.trace

theorem Test.PAM.cashflows_eq : cashflows = [((1, Actus.Protocol.EventType.IED), Actus.Contract.PAM.pof_IED pam rf 1), ((2, Actus.Protocol.EventType.MD), Actus.Contract.PAM.pof_MD rf 2 s1)]

The trace produces exactly the IED then MD cashflows.

theorem Test.PAM.md_zeroes_notional : s2.nt = 0

Maturity zeroes the notional (definitional).

def Test.PAM.pamDated : Actus.Contract.Terms Float

A dated 1-year bullet loan paying interest semi-annually.

Equations

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