Module formal_model 

Functions

add_saturating

dealer_sign

law_dealer_sign_is_pm_one

law_offsetting_legs_net_to_zero

law_orient_long_is_identity

negate_saturating

net_exposure

oriented_exposure