diff --git a/src/main/daml/ContingentClaims/Valuation/AcquisitionTime.daml b/src/main/daml/ContingentClaims/Valuation/AcquisitionTime.daml
new file mode 100644
index 000000000..b5de313cd
--- /dev/null
+++ b/src/main/daml/ContingentClaims/Valuation/AcquisitionTime.daml
@@ -0,0 +1,50 @@
+-- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+module ContingentClaims.Valuation.AcquisitionTime
+  ( AcquisitionTime(..)
+  , beforeOrAtToday
+  , extend
+  , isNever
+  ) where
+
+import ContingentClaims.Core.Claim (Inequality(..))
+import Prelude hiding (Time, sequence, mapA, const)
+
+-- | Acquisition time of a contract in the context of the valuation semantics.
+-- It is either a deterministic time (`Time t`) or it is defined based on a list of `Inequality`.
+-- For inequalities [i_1, i_2, ..., i_N], the acquisition time is defined as the first instant `t` for which there exist times `t_1 ≤ t_2 ≤ ... ≤ t_N ≤ t` such that `t_k` verifies `i_k` for each `k`.
+-- In both cases, the time `t` is a stopping time in the mathematical sense.
+data AcquisitionTime t x o
+  = Time t
+    -- ^ Acquisition at time `t`.
+  | AtInequality { inequalities : [Inequality t x o] }
+    -- ^ Acquisition when inequalities are verified. The order of the inequalities matters (see definition above).
+  | Never
+    -- ^ Acquisition never happens.
+  deriving (Eq,Show)
+
+-- | Given an inequality and an acquisition time τ1, it returns the acquisition time τ2 corresponding to the first instant such that
+-- - the inequality is verified
+-- - τ2 ≥ τ1
+-- The name `extend` comes from the fact that we are extending the set of inequality constraints that need to be verified.
+extend : (Ord t) => Inequality t x o -> AcquisitionTime t x o -> AcquisitionTime t x o
+extend _ Never = Never
+extend (TimeGte s) (Time t) = Time $ max s t
+extend (TimeLte s) (Time t) | s >= t = Time t
+extend (TimeLte s) (Time t) = Never
+extend ineq@(Lte _) (Time t) = AtInequality [TimeGte t, ineq]
+extend ineq (AtInequality ineqs) = AtInequality $ ineqs <> [ineq]
+
+-- | Checks if an acquisition time falls before or at the today date.
+-- `None` is returned if the acquisition time is unknown.
+beforeOrAtToday : (Ord t) => t -> AcquisitionTime t x a -> Optional Bool
+beforeOrAtToday _ Never = Some False
+beforeOrAtToday today (Time s) = Some $ s <= today
+beforeOrAtToday today (AtInequality _) = None
+
+-- | Checks if an acquisition time is `Never`.
+-- This is used to avoid requiring the (Eq o) constraint.
+isNever : AcquisitionTime t x a -> Bool
+isNever Never = True
+isNever _ = False
diff --git a/src/main/daml/ContingentClaims/Valuation/Expression.daml b/src/main/daml/ContingentClaims/Valuation/Expression.daml
new file mode 100644
index 000000000..80a31ec71
--- /dev/null
+++ b/src/main/daml/ContingentClaims/Valuation/Expression.daml
@@ -0,0 +1,212 @@
+-- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+module ContingentClaims.Valuation.Expression (
+  Expr(..),
+  ExprF(..),
+  simplify
+) where
+
+import ContingentClaims.Core.Claim (Inequality(..))
+import ContingentClaims.Valuation.AcquisitionTime(AcquisitionTime(..))
+import DA.Foldable
+import DA.Traversable
+import Daml.Control.Recursion
+import Prelude hiding (Time, sequence, mapA, const)
+
+-- | Represents an algebraic expression of a t-adapted stochastic process.
+-- t : time parameter.
+-- x : state parameter, typically Decimal (our best approximation of real numbers).
+-- o : reference used to identify observables.
+-- b : type describing elementary processes.
+data Expr t x o b
+  = Const x
+    -- ^ A constant process.
+  | Proc { name : b }
+    -- ^ An elementary process which we cannot decompose further.
+  -- | Sup { lowerBound: t, tau: t, rv : Expr t }
+    -- -- ^ Sup, needs to be reworked using feasible exercise strategies.
+  | Sum [Expr t x o b]
+    -- ^ Sum process.
+  | Neg (Expr t x o b)
+    -- ^ Negation process.
+  | Mul (Expr t x o b, Expr t x o b)
+    -- ^ Multiplication of two processes (`p1 * p2`).
+  | Inv (Expr t x o b)
+    -- ^ Inverse of a process (`1 / p`).
+  | Max [Expr t x o b]
+    -- ^ Maximum process.
+  | I (Inequality t x o)
+    -- ^ Indicator function. I(p) is 1 if p(t) = True, False otherwise, where
+    -- `p` is the boolean process corresponding to the provided inequality.
+    -- Specifically, this means
+    -- - for `o1 ≤ o2`, `p = υ(o1) ≤ υ(o2)`
+    -- - for `TimeGte t`, `p(s) = s ≥ t`
+    -- - for `TimeLte t`, `p(s) = s ≤ t`
+  | E { process : Expr t x o b, time : AcquisitionTime t x o, filtration : AcquisitionTime t x o }
+    -- ^ Conditional expectation of `process(time)` conditioned on the filtration F_`t`.
+  -- | Snell { process : Expr t x o b, time : AcquisitionTime t x o, predicate : Inequality t x o}
+  --     -- ^ Snell envelope of a stochastic process.
+  --     -- We need the predicate to identify the feasible region
+  --     -- I feel that we need the acquisition time to identify the conditional filtration, but it might not be needed.
+  -- | Absorb { process : Expr t x o b, time : AcquisitionTime t x o, predicate : Inequality t x o}
+  --     -- ^ Absorb primitive.
+  --     -- It feels that absorb hides an expectation, but I need to write this down in formulas for better understanding.
+  -- In order to write until valuation explicitly, we need to introduce a new class of boolean processes, namely those that we start observing at a time tau and have never been true since (we can then use an indicator function to transform it to a real process)
+  -- We can use the absorb primitive to cover this case, which we can then distribute. across the other primitives.
+  deriving (Eq,Show)
+
+-- | Base functor for `Expr`.
+data ExprF t x o b c
+  = ConstF x
+  | ProcF { name : b }
+  -- | Sup { lowerBound: t, tau: t, rv : Expr t }
+  | SumF [c]
+  | NegF c
+  | MulF { lhs : c, rhs : c }
+  | InvF c
+  | MaxF [c]
+  | I_F (Inequality t x o)
+  | E_F { process : c, time : AcquisitionTime t x o, filtration : AcquisitionTime t x o }
+  deriving (Functor)
+
+instance Recursive (Expr t x o b) (ExprF t x o b) where
+  project (Const d) = ConstF d
+  project Proc{..} = ProcF with ..
+  -- project Sup{..} = SupF with ..
+  project (Sum xs) = SumF xs
+  project (Neg x) = NegF x
+  project (Mul (x,x')) = MulF x x'
+  project (Inv x) = InvF x
+  project (Max xs) = MaxF xs
+  project (I x) = I_F x
+  project E{..} = E_F with ..
+
+instance Corecursive (Expr t x o b) (ExprF t x o b) where
+  embed (ConstF d) = Const d
+  embed ProcF{..} = Proc with ..
+  -- embed SupF{..} = Sup with ..
+  embed (SumF xs) = Sum xs
+  embed (NegF x) = Neg x
+  embed (MulF x x') = Mul (x, x')
+  embed (InvF x) = Inv x
+  embed (MaxF xs) = Max xs
+  embed (I_F x) = I x
+  embed E_F{..} = E with ..
+
+instance Foldable (ExprF t x o b) where
+  foldMap f (ConstF _) = mempty
+  foldMap f (ProcF _) = mempty
+  -- foldMap f (SupF _ _ x) = f x
+  foldMap f (SumF xs) = foldMap f xs
+  foldMap f (NegF x) = f x
+  foldMap f (MulF x x') = f x <> f x'
+  foldMap f (InvF x) = f x
+  foldMap f (MaxF xs) = foldMap f xs
+  foldMap f (I_F _) = mempty
+  foldMap f (E_F x _ _) = f x
+
+instance Traversable (ExprF t x o b) where
+  sequence (ConstF d) = pure $ ConstF d
+  sequence (ProcF x) = pure $ ProcF x
+--   sequence (SupF t τ fa) = SupF t τ <$> fa
+  sequence (SumF [fa]) = (\a -> SumF [a]) <$> fa
+  sequence (SumF (fa :: fas)) = s <$> fa <*> sequence fas
+    where s a as = SumF (a :: as)
+  sequence (SumF []) = error "Traversable ExprF: sequence empty SumF"
+  sequence (NegF fa) = NegF <$> fa
+  sequence (MulF fa fa') = MulF <$> fa <*> fa'
+  sequence (InvF fa) = InvF <$> fa
+  sequence (MaxF (fa :: fas)) = s <$> fa <*> sequence fas
+    where s a as = MaxF (a :: as)
+  sequence (MaxF []) = error "Traversable ExprF: sequence empty MaxF"
+  sequence (I_F p) = pure $ I_F p
+  sequence (E_F fa t f) = (\a -> E_F a t f) <$> fa
+
+instance (Additive x) => Additive (Expr t x o b) where
+  x + y = Sum [x, y]
+  negate = Neg
+  aunit = Const aunit
+
+instance (Multiplicative x) => Multiplicative (Expr t x o b) where
+  (*) = curry Mul
+  munit = Const munit
+  x ^ y | y > 0 = x * (x ^ pred y)
+  x ^ 0 = munit
+  x ^ y = Inv x ^ (-y)
+
+instance (Multiplicative x) => Divisible (Expr t x o b) where
+  x / y = curry Mul x $ Inv y
+
+-- | This is meant to be a function that algebraically simplifies the FAPF by
+-- 1) using simple identities and ring laws
+-- 2) change of numeraire technique.
+simplify : (Eq x, Eq b, Eq t, Eq o, Multiplicative x) => Expr t x o b -> Expr t x o b
+simplify =
+    cata unitIdentity
+  -- . cata zeroIdentity
+  . cata factNeg
+  -- . \case [] -> Const aunit
+  --         [x] -> x
+  --         xs -> Sum xs
+  -- . cata distSum
+  -- . ana commuteLeft
+  -- . cata mulBeforeSum
+
+-- {- Functions below here are helpers for simplifying the expression tree, used mainly in `simplify` -}
+
+-- | Algebra that simplifies sums, multiplications, expectations involving 0.0.
+-- BUG I need to add an additive typeclass constraint, otherwise aunit is just a pattern match.
+zeroIdentity : ExprF t x o b (Expr t x o b) -> Expr t x o b
+zeroIdentity (MulF (Const aunit) x) = Const aunit
+zeroIdentity (MulF x (Const aunit)) = Const aunit
+zeroIdentity (SumF xs) = Sum $ filter (not . isZero) xs
+  where isZero (Const aunit) = True
+        isZero _ = False
+zeroIdentity (E_F (Const aunit) _ _) = Const aunit
+zeroIdentity other = embed other
+
+-- | Algebra that simplifies multiplications and divisions by 1.0.
+unitIdentity : (Eq x, Eq b, Eq t, Eq o, Multiplicative x) => ExprF t x o b (Expr t x o b) -> Expr t x o b
+unitIdentity (MulF a b) | a == munit = b
+unitIdentity (MulF a b) | b == munit = a
+unitIdentity (InvF x) | x == munit = munit
+unitIdentity other = embed other
+
+-- | Algebra that collects and simplifies minuses.
+factNeg : ExprF t x o b (Expr t x o b) -> Expr t x o b
+factNeg (NegF (Neg x)) = x
+-- factNeg (MulF (Neg x) (Neg y)) = Mul (x, y) -- [ML] I think this is redundant
+factNeg (MulF (Neg x) y) = Neg $ Mul (x, y)
+factNeg (MulF y (Neg x)) = Neg $ Mul (y, x)
+factNeg (E_F (Neg x) t f) = Neg $ E x t f
+factNeg other = embed other
+
+-- -- | Turn any expression into a list of terms to be summed together
+-- distSum : ExprF t x o b [Expr t x o b] -> [Expr t x o b]
+-- distSum = \case
+--   ConstF x -> [Const x]
+--   SumF xs -> join xs
+--   MulF xs xs' -> curry Mul <$> xs <*> xs'
+--   NegF xs -> Neg <$> xs
+--   E_F xs t -> flip E t <$> xs
+--   I_F xs xs' -> [I (unroll xs, unroll xs')]
+--   ProcF{..} -> [Proc{..}]
+--   where unroll xs = Sum xs
+
+-- | Algebra that changes `(a + b) x c` to `c x (a + b)`
+-- mulBeforeSum : ExprF t x o b (Expr t x o b) -> Expr t x o b
+-- mulBeforeSum (MulF y@Sum{} x) = Mul (x, y)
+-- mulBeforeSum (MulF (Mul (x, y@Sum{})) x') = Mul (Mul (x,x'), y)
+-- mulBeforeSum other = embed other
+
+-- | Algebra that applies commutative property to all multiplications.
+-- commute : ExprF t x o b (Expr t x o b) -> Expr t x o b
+-- commute (MulF a b) = embed $ MulF b a
+-- commute other = embed other
+
+-- | Change e.g. `a x (b x c)` to `(a x b) x c`.
+-- We are not using commutative property, but rather associative --> should rename
+-- commuteLeft : Expr t x o b -> ExprF t x o b (Expr t x o b)
+-- commuteLeft (Mul (a,(Mul (b, c)))) = Mul (a, b) `MulF` c
+-- commuteLeft other = project other
diff --git a/src/main/daml/ContingentClaims/Valuation/Stochastic.daml b/src/main/daml/ContingentClaims/Valuation/Stochastic.daml
index ab469dfea..55a104943 100644
--- a/src/main/daml/ContingentClaims/Valuation/Stochastic.daml
+++ b/src/main/daml/ContingentClaims/Valuation/Stochastic.daml
@@ -11,8 +11,6 @@ module ContingentClaims.Valuation.Stochastic (
   , fapf
   , gbm
   , riskless
-  , simplify
-  , unitIdentity
 ) where
 
 import ContingentClaims.Core.Internal.Claim (Claim(..), Inequality(..))
@@ -30,10 +28,10 @@ import Prelude hiding (Time, sequence, mapA, const)
 -- dX / X = α dt + β dW. Eventually, we wish to support other processes such as Levy.
 data Process t = Process { dt : Expr t, dW: Expr t } deriving (Show, Eq)
 
--- | Helper function to create a riskless process `dS = r dt`.
+-- | Helper function to create a riskless process `dS = r dt`
 riskless r = Process { dt = Ident r, dW = Const 0.0 }
 
--- | Helper function to create a geometric BM `dS = μ dt + σ dW`.
+-- | Helper function to create a geometric BM `dS = μ dt + σ dW`
 gbm μ σ = Process { dt = Ident μ, dW = Ident σ }
 
 -- | Base functor for `Expr`. Note that this is ADT is re-used in a couple of places, e.g.,
@@ -51,7 +49,7 @@ data ExprF t x
   | E_F { rv : x, filtration: t }
   deriving (Functor)
 
--- | Represents an expression of t-adapted stochastic processes.
+-- | Represents an expression of t-adapted stochastic processes
 data Expr t
   = Const Decimal
   | Ident t
@@ -90,7 +88,7 @@ instance Corecursive (Expr t) (ExprF t) where
   embed E_F{..} = E with ..
 
 class IsIdentifier t where
-  -- | Produce a local identifier of type `t`, subindexed by `i`.
+  -- | Produce a local identifier of type `t`, subindexed by `i`
   localVar : Int -> t
 
 instance Foldable (ExprF t) where
@@ -125,16 +123,16 @@ instance Traversable (ExprF t) where
 -- one-to-one to the formulae in our whitepaper. This is still an experimental feature.
 fapf : (Eq a, Show a, Show o, IsIdentifier t)
      => a
-       -- ^ Currency in which the value process is expressed.
+       -- ^ Currency in which the value process is expressed
      -> (a -> Process t)
-       -- ^ Maps a currency to the corresponding discount factor process.
+       -- ^ Maps a currency to the corresponding discount factor process
      -> (a -> a -> Process t)
        -- ^ Given an asset and a currency, it returns the value process of the asset expressed in
       --    units of currency.
      -> (o -> Process t)
-       -- ^ Given an observable, it returns its value process.
+       -- ^ Given an observable, it returns its value process
      -> t
-       -- ^ The today date.
+       -- ^ today date
      -> Claim t Decimal a o -> Expr t
 fapf ccy disc exch val today = flip evalState 0 . futuM coalg . Left . (, today) where
   -- coalg : (Either (Claim, t) (Observable, t)) ->
@@ -189,72 +187,3 @@ fapf ccy disc exch val today = flip evalState 0 . futuM coalg . Left . (, today)
   val' obs t = ProcF (show obs) (val obs) t
   one = munit
   zero = aunit
-
--- | This is meant to be a function that algebraically simplifies the FAPF by
--- 1) using simple identities and ring laws
--- 2) change of numeraire technique.
--- This is still an experimental feature.
-simplify : Expr t -> Expr t
-simplify =
-    cata unitIdentity
-  . cata zeroIdentity
-  . cata factNeg
-  . \case [] -> Const aunit
-          [x] -> x
-          xs -> Sum xs
-  . cata distSum
-  . ana commuteLeft
-  . cata mulBeforeSum
-
-{- Functions below are helpers for simplifying the expression tree, used mainly in `simplify` -}
-
-zeroIdentity : ExprF t (Expr t) -> Expr t
-zeroIdentity (MulF (Const 0.0) x) = Const 0.0
-zeroIdentity (MulF x (Const 0.0)) = Const 0.0
-zeroIdentity (PowF x (Const 0.0)) = Const 1.0
-zeroIdentity (SumF xs) = Sum $ filter (not . isZero) xs
-  where isZero (Const 0.0) = True
-        isZero _ = False
-zeroIdentity (E_F (Const 0.0) _) = Const 0.0
-zeroIdentity other = embed other
-
--- | HIDE
-unitIdentity : ExprF t (Expr t) -> Expr t
-unitIdentity (MulF (Const 1.0) x) = x
-unitIdentity (MulF x (Const 1.0)) = x
-unitIdentity (PowF x (Const 1.0)) = x
-unitIdentity other = embed other
-
-factNeg : ExprF t (Expr t) -> Expr t
-factNeg (NegF (Neg x)) = x
-factNeg (MulF (Neg x) (Neg y)) = Mul (x, y)
-factNeg (MulF (Neg x) y) = Neg $ Mul (x, y)
-factNeg (MulF y (Neg x)) = Neg $ Mul (y, x)
-factNeg (E_F (Neg x) t) = Neg $ E x t
-factNeg other = embed other
-
--- | Turn any expression into a list of terms to be summed together
-distSum : ExprF t [Expr t] -> [Expr t]
-distSum = \case
-  ConstF x -> [Const x]
-  IdentF x -> [Ident x]
-  SumF xs -> join xs
-  MulF xs xs' -> curry Mul <$> xs <*> xs'
-  NegF xs -> Neg <$> xs
-  E_F xs t -> flip E t <$> xs
-  I_F xs xs' -> [I (unroll xs, unroll xs')]
-  PowF xs is -> [Pow (unroll xs, unroll is)]
-  ProcF{..} -> [Proc{..}]
-  SupF t τ xs -> [Sup t τ (unroll xs)]
-  where unroll xs = Sum xs
-
--- | Change `(a + b) x c` to `c x (a + b)`
-mulBeforeSum : ExprF t (Expr t) -> Expr t
-mulBeforeSum (MulF y@Sum{} x) = Mul (x, y)
-mulBeforeSum (MulF (Mul (x, y@Sum{})) x') = Mul (Mul (x,x'), y)
-mulBeforeSum other = embed other
-
--- | Change e.g. `a x (b x c)` to `(a x b) x c`
-commuteLeft : Expr t -> ExprF t (Expr t)
-commuteLeft (Mul (x,(Mul (a, b)))) = Mul (x, a) `MulF` b
-commuteLeft other = project other
diff --git a/src/main/daml/ContingentClaims/Valuation/Stochastic2.daml b/src/main/daml/ContingentClaims/Valuation/Stochastic2.daml
new file mode 100644
index 000000000..51c9cdef6
--- /dev/null
+++ b/src/main/daml/ContingentClaims/Valuation/Stochastic2.daml
@@ -0,0 +1,137 @@
+-- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+module ContingentClaims.Valuation.Stochastic2 (
+  ElementaryProcess(..),
+  fapf,
+) where
+
+import ContingentClaims.Core.Claim hiding ((<=))
+import ContingentClaims.Core.Internal.Claim (Claim(..))
+import ContingentClaims.Core.Observation qualified as O
+import ContingentClaims.Core.Util.Recursion (futuM)
+import ContingentClaims.Valuation.AcquisitionTime(AcquisitionTime(..), beforeOrAtToday, extend, isNever)
+import ContingentClaims.Valuation.Expression
+import Daml.Control.Arrow ((|||))
+import Daml.Control.Recursion
+import Prelude hiding (compare)
+
+-- | Elementary processes as described in the Peyton-Jones paper.
+-- Once a model assumption is made, these can be replaced by the specific model (e.g. geometric brownian motion for stock spot prices).
+data ElementaryProcess a o
+  = Observable o
+      -- ^ Process corresponding to an observable.
+  | Exch with { asset : a, currency : a }
+      -- ^ Value of `asset` expressed in units of `currency`.
+  | Disc a
+      -- ^ Discount factor expressed in currency `a`.
+  deriving (Eq, Show)
+
+-- | Maps a claim to the corresponding value process in currency `ccy`, taking into account known information up to time `t`.
+fapf : (Ord t, Eq a, Ord x, Number x, Divisible x, CanAbort m)
+  => (o -> t -> m x)
+    -- ^ Function to evaluate observables.
+  -> a
+    -- ^ Currency.
+  -> t
+    -- ^ Valuation date.
+  -> t
+    -- ^ The claim's (known) acquisition time.
+  -> Claim t x a o
+    -- ^ The input claim.
+  -> m (Expr t x o (ElementaryProcess a o))
+fapf spot ccy t acquisitionTime claim =
+  futuM coalg
+  $ Left (claim, Time acquisitionTime) -- `Left` is used for claims, `Right` for observables
+  where
+    -- coalg : (Additive x) => (Carrier t x a) -> (ExprF t x a (ElementaryProcess a) (Free (ExprF t x a (ElementaryProcess a)) (Carrier t x a)))
+    coalg = ϵ spot t ccy ||| υ
+    -- υ : (O.Observation t x a, AcquisitionTime t x a) -> (ExprF t x a (ElementaryProcess a) (Free (ExprF t x a (ElementaryProcess a)) (Carrier t x a)))
+    υ (O.Const {value=k}, _) = pure $ ConstF k
+    υ (O.Observe {key=observable}, Time s) | s <= t = ConstF <$> spot observable s
+    υ (O.Observe {key=observable}, s) = pure . ProcF $ Observable observable
+    υ (O.Add (x, x'), s) = pure $ SumF [obs (x, s), obs (x', s)]
+    υ (O.Neg x, s) =  pure . NegF $ obs (x, s)
+    υ (O.Mul (x, x'), s) = pure $ obs (x, s) `MulF` obs (x', s)
+    υ (O.Div (x, x'), t) = pure $ obs (x, t) `MulF` inv (obs (x', t))
+    obs = pure . Right
+    inv = Free . InvF
+
+-- | HIDE
+-- Valuation semantics for a `Claim`.
+ϵ : (Eq a, Ord t, Ord x, Number x, Divisible x, CanAbort m)
+  => (o -> t -> m x)
+    -- ^ Function to evaluate observables.
+  -> t
+    -- ^ Valuation date.
+  -> a
+    -- ^ Currency.
+  -> (Claim t x a o, AcquisitionTime t x o)
+    -- ^ The input claim and its acquisition time.
+  -> m (ExprF t x o (ElementaryProcess a o) (Free (ExprF t x o (ElementaryProcess a o)) (Carrier t x a o)))
+-- Zero
+ϵ _ _ _ (Zero, _) = pure $ ConstF aunit
+-- One
+ϵ _ _ ccy (One asset, _) = pure $ exch asset ccy
+  where
+    exch asset ccy = if asset == ccy then ConstF munit else ProcF $ Exch asset ccy
+-- Give
+ϵ _ _ _ (Give c, s) = pure . NegF $ Pure $ Left (c,s)
+-- Scale
+ϵ _ _ _ (Scale k c, s) = pure $ obs (k,s) `MulF` claim (c,s)
+  where obs = pure . Right
+        claim = pure . Left
+-- And
+ϵ _ _ _ (And c c' cs, s) = pure . SumF $ fmap (claim . (, s)) (c :: c' :: cs)
+  where claim = pure . Left
+-- Or
+ϵ _ _ _ (Or c c' cs, s) = pure . MaxF $ fmap (claim . (, s)) (c :: c' :: cs)
+  where claim = pure . Left
+-- When, the acquisition time of the inner contract is known and not in the future
+ϵ spot t ccy (When pred c, s) | beforeOrAtToday t τ == Some True = ϵ spot t ccy (c, τ)
+  where τ = extend pred s
+-- When, the acquisition time of the inner contract never happens
+ϵ spot t ccy (When pred c, s) | isNever τ = pure $ ConstF aunit
+  where τ = extend pred s
+-- When, the acquisition time of the inner contract is either unknown or known but in the future
+ϵ _ t ccy (When pred c, s) = pure $ MulF (ex (disc * claim (c,τ)) τ filtration) $ inv disc
+  where τ = extend pred s
+        filtration = case s of
+          AtInequality _ -> s -- acquisition time of the outer contract is unknown
+          other -> extend (TimeGte t) s -- acquisition time of the outer contract is known
+        claim = pure . Left
+        disc = Free . ProcF $ Disc ccy
+        x * y = Free $ MulF x y
+        ex e τ f = Free $ E_F e τ f
+        inv = Free . InvF
+-- Cond, the acquisition time of the inner contract is known and not in the future
+ϵ spot t ccy (Cond pred c1 c2, Time s) | s <= t = do
+  predicate <- compare spot pred s
+  if predicate then ϵ spot t ccy (c1, Time s) else ϵ spot t ccy (c2, Time s)
+-- Cond, the acquisition time is either unknown or known but in the future
+ϵ spot t ccy (Cond pred c1 c2, s) =
+  let
+    v1 = ind pred * claim (c1,s)
+    v2 = (one - ind pred) * claim (c2,s)
+  in
+    pure $ SumF [v1, v2]
+  where claim = pure . Left
+        x - y = Free $ SumF [x, (Free $ NegF y)]
+        x * y = Free $ MulF x y
+        ind = Free . I_F
+        one = Free $ ConstF munit
+-- Until
+ϵ _ _ _ (Until _ _, _) = abort "Valuation semantics for `Until` is not supported yet."
+-- Anytime
+ϵ _ _ _ (Anytime _ _, _) = abort "Valuation semantics for `Anytime` is not supported yet."
+
+-- TODO : handle `Never` acquisition time which could originate from using `TimeLte`. We probably need to use resolve at every step.
+
+-- | HIDE
+-- Carrier of the CV-coalgebra ϵ ||| υ
+type Carrier t x a o = Either (Claim t x a o, AcquisitionTime t x o) (O.Observation t x o, AcquisitionTime t x o)
+
+
+
+
+
diff --git a/src/test/daml/ContingentClaims/Test/Pricing.daml b/src/test/daml/ContingentClaims/Test/Pricing.daml
index 95b708e9a..a5628fa50 100644
--- a/src/test/daml/ContingentClaims/Test/Pricing.daml
+++ b/src/test/daml/ContingentClaims/Test/Pricing.daml
@@ -1,116 +1,110 @@
 -- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
 -- SPDX-License-Identifier: Apache-2.0
 
-module ContingentClaims.Test.Pricing where
-
-import ContingentClaims.Core.Builders (european)
-import ContingentClaims.Core.Claim
-import ContingentClaims.Core.Observation qualified as O
-import ContingentClaims.Valuation.MathML qualified as MathML
-import ContingentClaims.Valuation.Stochastic (Expr(..), IsIdentifier(..), fapf, gbm, riskless, {- simplify, -} unitIdentity)
-import DA.Assert
-import Daml.Control.Recursion (cata)
-import Daml.Script
-import Prelude hiding (max)
-
-data Instrument = USD | EUR | AMZN | APPL deriving (Show, Eq)
-
-data Observable = Spot_AMZN | Spot_APPL deriving (Show, Eq)
-
-spot : Instrument -> Observable
-spot AMZN = Spot_AMZN
-spot APPL = Spot_APPL
-spot other = error $ "disc: " <> show other
-
-call : Instrument -> Decimal -> Instrument -> Claim t Decimal Instrument Observable
-call s k a = scale (O.observe (spot s) - O.pure k) $ one a
-
-margrabe s1 s2 a = scale (O.observe (spot s1) - O.observe (spot s2)) $ one a
-
-disc USD = riskless "r_USD"
-disc EUR = riskless "r_EUR"
-disc other = error $ "disc: " <> show other
-
-val Spot_AMZN = gbm "μ_AMZN" "σ_AMZN"
-val Spot_APPL = gbm "μ_APPL" "σ_APPL"
-
-exch a a' = error $ "exch: " <> show a <> "/" <> show a'
-
-t = "t"  -- today
-t' = "T" -- maturity
-
-instance IsIdentifier Text where
-  localVar i = "τ_" <> show i
-
-instance Additive (Expr t) where
-  x + y = Sum [x, y]
-  negate = Neg
-  aunit = Const 0.0
-
-instance Multiplicative (Expr t) where
-  (*) = curry Mul
-  x ^ y = curry Pow x $ Const (intToDecimal y)
-  munit = Const 1.0
-
-instance Divisible (Expr t) where
-  x / y = curry Mul x . curry Pow y . Neg . Const $ 1.0
-
-instance Number (Expr t) where
-
-max x y = I (x, y) * x + I (y, x) * y
-
--- This is needed because scale x (one USD) = x * 1.0. It would make writing the expressions by hand
--- tedious
-multIdentity = cata unitIdentity
-
--- Helper to compare the output in XML format (paste this into a browser)
-print f e = do
-  debug $ "Formula:" <> prnt f
-  debug $ "Expected:" <> prnt e
-  where prnt = show . MathML.presentation {- . simplify -}
-
-valueCall = script do
-  let
-    formula = fapf USD disc exch val t $ european t' (call AMZN 3300.0 USD)
-    s = Proc "Spot_AMZN" (val Spot_AMZN)
-    k = Const 3300.0
-    usd = Proc "USD" (disc USD)
-    expect = usd t * E (max (s t' - k) aunit / usd t') t
-  print formula expect
-  multIdentity formula === expect
-
-valueMargrabe = script do
-  let
-    formula = fapf USD disc exch val t $ european t' (margrabe AMZN APPL USD)
-    s = Proc "Spot_AMZN" (val Spot_AMZN)
-    s' = Proc "Spot_APPL" (val Spot_APPL)
-    usd = Proc "USD" (disc USD)
-    expect = usd t * E (max (s t' - s' t') aunit / usd t') t
-  print formula expect
-  multIdentity formula === expect
-
--- valueAmerican = script do
---   let
---     formula = fapf USD disc exch t $ american t t' (call APPL 142.50 USD)
---     s = Proc "APPL" (exch APPL USD)
---     k = Const 142.50
---     usd = Proc "USD" (disc USD)
---     τ = "τ_0"
---     expect = Sup t τ (usd t * E (max (s τ - k) aunit * I (Ident τ, Ident t') / usd τ ) t)
+module Test.Pricing where
+
+-- import ContingentClaims.Claim
+-- import ContingentClaims.Financial (european, american)
+-- import ContingentClaims.Observation qualified as O
+-- import ContingentClaims.MathML qualified as MathML
+-- import ContingentClaims.Math.Stochastic (fapf, {- simplify, -} riskless, gbm, Expr(..), IsIdentifier(..))
+-- import Daml.Control.Recursion (cata)
+
+-- import Daml.Script
+-- import DA.Assert
+-- import Prelude hiding (max)
+
+-- data Instrument = USD | EUR | AMZN | APPL deriving (Show, Eq)
+
+-- data Observable = Spot_AMZN | Spot_APPL deriving (Show, Eq)
+
+-- spot : Instrument -> Observable
+-- spot AMZN = Spot_AMZN
+-- spot APPL = Spot_APPL
+-- spot other = error $ "disc: " <> show other
+
+-- call : Instrument -> Decimal -> Instrument -> Claim t Decimal Instrument Observable
+-- call s k a = scale (O.observe (spot s) - O.pure k) $ one a
+
+-- margrabe s1 s2 a = scale (O.observe (spot s1) - O.observe (spot s2)) $ one a
+
+-- disc USD = riskless "r_USD"
+-- disc EUR = riskless "r_EUR"
+-- disc other = error $ "disc: " <> show other
+
+-- val Spot_AMZN = gbm "μ_AMZN" "σ_AMZN"
+-- val Spot_APPL = gbm "μ_APPL" "σ_APPL"
+
+-- exch a a' = error $ "exch: " <> show a <> "/" <> show a'
+
+-- t = "t"  -- today
+-- t' = "T" -- maturity
+
+-- instance IsIdentifier Text where
+--   localVar i = "τ_" <> show i
+
+-- instance Additive (Expr t) where
+--   x + y = Sum [x, y]
+--   negate = Neg
+--   aunit = Const 0.0
+
+-- instance Multiplicative (Expr t) where
+--   (*) = curry Mul
+--   x ^ y = curry Pow x $ Const (intToDecimal y)
+--   munit = Const 1.0
+
+-- instance Divisible (Expr t) where
+--   x / y = curry Mul x . curry Pow y . Neg . Const $ 1.0
+
+-- instance Number (Expr t) where
+
+-- max x y = I (x, y) * x + I (y, x) * y
+
+-- -- This is needed because scale x (one USD) = x * 1.0. It would make writing
+-- -- the expressions by hand tedious
+-- multIdentity = cata unitIdentity
+
+-- -- Helper to compare the output in XML format (paste this into a browser)
+-- print f e = do debug $ "Formula:" <> prnt f
+--                debug $ "Expected:" <> prnt e
+--   where prnt = show . MathML.presentation {- . simplify -}
+
+-- valueCall = script do
+--   let formula = fapf USD disc exch val t $ european t' (call AMZN 3300.0 USD)
+--       s = Proc "Spot_AMZN" (val Spot_AMZN)
+--       k = Const 3300.0
+--       usd = Proc "USD" (disc USD)
+--       expect = usd t * E (max (s t' - k) aunit / usd t') t
+--   print formula expect
+--   multIdentity formula === expect
+
+-- valueMargrabe = script do
+--   let formula = fapf USD disc exch val t $ european t' (margrabe AMZN APPL USD)
+--       s = Proc "Spot_AMZN" (val Spot_AMZN)
+--       s' = Proc "Spot_APPL" (val Spot_APPL)
+--       usd = Proc "USD" (disc USD)
+--       expect = usd t * E (max (s t' - s' t') aunit / usd t') t
 --   print formula expect
 --   multIdentity formula === expect
 
--- Check to see that the subscript numbering works
-testMonadicBind = script do
-  let
-    τ₀ = "τ_0"
-    τ₁ = "τ_1"
-    t₀ = "t_0"
-    t₁ = "t_1"
-    usd = Proc "USD" (disc USD)
-    formula = fapf USD disc exch val t $ anytime (TimeGte t₀) (anytime (TimeGte t₁) (one USD))
-    expect =
-      -- note the innermost 1/USD_τ₁ is mult identity
-      Sup t₀ τ₀ (usd t * E (Sup t₁ τ₁ (usd τ₀ * E (munit / usd τ₁) τ₀) / usd τ₀) t)
-  print formula expect
-  multIdentity formula === multIdentity expect
+-- -- valueAmerican = script do
+-- --   let formula = fapf USD disc exch t $ american t t' (call APPL 142.50 USD)
+-- --       s = Proc "APPL" (exch APPL USD)
+-- --       k = Const 142.50
+-- --       usd = Proc "USD" (disc USD)
+-- --       τ = "τ_0"
+-- --       expect = Sup t τ (usd t * E (max (s τ - k) aunit * I (Ident τ, Ident t') / usd τ ) t)
+-- --   print formula expect
+-- --   multIdentity formula === expect
+
+-- -- Check to see that the subscript numbering works
+-- testMonadicBind = script do
+--   let τ₀ = "τ_0"
+--       τ₁ = "τ_1"
+--       t₀ = "t_0"
+--       t₁ = "t_1"
+--       usd = Proc "USD" (disc USD)
+--       formula = fapf USD disc exch val t $ anytime (TimeGte t₀) (anytime (TimeGte t₁) (one USD))
+--       expect = Sup t₀ τ₀ (usd t * E (Sup t₁ τ₁ (usd τ₀ * E (munit / usd τ₁) τ₀) / usd τ₀) t) -- note the innermost 1/USD_τ₁ is mult identity
+--   print formula expect
+--   multIdentity formula === multIdentity expect
diff --git a/src/test/daml/ContingentClaims/Test/Pricing2.daml b/src/test/daml/ContingentClaims/Test/Pricing2.daml
new file mode 100644
index 000000000..b01bdbd86
--- /dev/null
+++ b/src/test/daml/ContingentClaims/Test/Pricing2.daml
@@ -0,0 +1,197 @@
+-- Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+-- SPDX-License-Identifier: Apache-2.0
+
+module Test.Pricing2 where
+
+import ContingentClaims.Core.Builders (european)
+import ContingentClaims.Core.Claim
+import ContingentClaims.Core.Observation qualified as O
+import ContingentClaims.Valuation.AcquisitionTime
+import ContingentClaims.Valuation.Expression
+import ContingentClaims.Valuation.Stochastic2
+
+import Daml.Script
+import DA.Assert
+import DA.Date
+import DA.Tuple (thd3)
+import Prelude hiding (or, max, (<=))
+
+-- | Assets.
+data Instrument = USD | A | B | C deriving (Eq, Show)
+
+-- | Observables.
+data Observable = Spot_AMZN deriving (Eq, Show)
+
+-- | The claim type used for the tests.
+type C = Claim Date Decimal Instrument Observable
+
+-- | The observation type used for the tests.
+type O = O.Observation Date Decimal Observable
+
+-- Assets
+[ccy, a, b, c] = [USD, A, B, C]
+
+-- Dates
+t0 = date 1970 Jan 1
+t1 = succ t0
+t2 = succ t1
+
+-- Observations
+two : O = O.pure 2.0
+spotAmzn = O.observe Spot_AMZN
+
+-- Functions performing observations
+observe25: Observable -> Date -> Script Decimal = const . const . pure $ 25.0
+observeDayOfMonth _ d = pure . intToDecimal . thd3 . toGregorian $ d
+
+-- Inequalities
+false = TimeGte $ date 3000 Jan 1
+true = TimeGte $ date 1970 Jan 1
+atT1 = TimeGte t1
+
+-- Helper expressions
+disc = Proc $ Disc ccy
+exch = Proc $ Exch a ccy
+
+-- | Valuation of `One`, `Zero`, `Give`, `And`, `Or` nodes.
+testValuationBasic : Script()
+testValuationBasic = do
+
+  value <- fapf observe25 ccy t0 t0 (one a)
+  value === exch
+
+  value <- fapf observe25 ccy t0 t0 (one ccy)
+  value === Const 1.0
+
+  value <- fapf observe25 ccy t0 t0 zero
+  value === Const 0.0
+
+  value <- fapf observe25 ccy t0 t0 $ give (one a)
+  value === -exch
+
+  value <- fapf observe25 ccy t0 t0 $ one a <> one b <> one c
+  value === Sum [exch, Proc (Exch b ccy), Proc (Exch c ccy)]
+
+  value <- fapf observe25 ccy t0 t0 $ one a `or` one b
+  value === Max [exch, Proc (Exch b ccy)]
+
+  pure ()
+
+-- | Valuation of `When` nodes.
+testValuationWhen : Script()
+testValuationWhen = do
+  -- 1. When (TimeGte t) c
+  let
+    c1 = when atT1 $ one a
+    expect = E (disc * exch) τ f / disc
+        where
+          f = Time t0 -- filtration (i.e. available information)
+          τ = Time t1 -- stopping time defined by the `When` node
+
+  -- At `t0` the stopping rule defined by `When` is not verified, so we take expectation of discounted payoff
+  value <- fapf observe25 ccy t0 t0 c1
+  value === expect
+
+  -- At `t1` the stopping rule is verified, so we get rid of the `When` node
+  value <- fapf observe25 ccy t1 t0 c1
+  value === exch
+
+  -- 2. When (o1 <= o2) c
+  let
+    pred = O.Const 100.0 <= spotAmzn -- spot greater or equal than 100.0
+    c2 = when pred $ one a
+
+    f = Time t0 -- filtration
+    τ = AtInequality [TimeGte t0, pred] -- stopping rule
+
+  value <- fapf observe25 ccy t0 t0 c2
+  value === E (disc * exch) τ f / disc
+
+  -- We do not consider the case when the stopping rule is verified before or at t,
+  -- given that the valuation focuses on claims that are "up-to-date" with respect to lifecycle events
+  -- and the lifecycle function replaces verified stochastic stopping rule with deterministic ones
+
+  -- 3. When (TimeLte t) c
+  let
+    c3 = when (upTo t0) $ one a
+
+  -- Contract is acquired at `t0`, predicate is verified immediately
+  value <- fapf observe25 ccy t0 t0 c3
+  value === exch
+
+  -- Contract is acquired at `t1`, predicate is never verified
+  value <- fapf observe25 ccy t1 t1 c3
+  value === aunit
+
+-- | Valuation of `Scale` nodes.
+testValuationScale : Script()
+testValuationScale = do
+  let
+    observable  = O.Const 5.0 + spotAmzn
+    claim : C = when atT1 $ scale observable $ one a
+
+    f = Time t0 -- filtration
+    τ = Time t1 -- stopping rule
+    obsProcess = Const 5.0 + Proc (Observable Spot_AMZN)
+    expect = E (disc * (obsProcess * exch) ) τ f / disc
+
+  -- At `t0` the stopping rule is not verified
+  value <- fapf observe25 ccy t0 t0 claim
+  value === expect
+
+  -- At `t1` the stopping rule is verified
+  value <- fapf observe25 ccy t1 t0 claim
+  value === (Const 5.0 + Const 25.0) * exch
+
+  pure ()
+
+-- | Valuation of `Cond` nodes.
+testValuationCond : Script()
+testValuationCond = do
+  let
+    p1 = O.Const 5.0 <= spotAmzn
+    c1 : C = when atT1 $ cond p1 (one a) zero
+    p2 = spotAmzn <= O.Const 5.0
+    c2 : C = when atT1 $ cond p2 (one a) zero
+
+    f = Time t0 -- filtration
+    τ = Time t1 -- stopping rule
+    expect = E (disc * (I p1 * exch + (Const 1.0 - I p1) * aunit) ) τ f / disc
+
+  -- At `t0` the stopping rule is not verified
+  value <- fapf observe25 ccy t0 t0 c1
+  value === expect
+
+  -- At `t1` the stopping rule is verified
+  value <- fapf observe25 ccy t1 t0 c1
+  value === exch
+
+  value <- fapf observe25 ccy t1 t0 c2
+  value === aunit
+
+  pure ()
+
+valueCall = script do
+  let
+    k = O.pure 100.0 -- strike price
+    c : C = european t1 $ scale (spotAmzn - k) $ one USD
+    f = Time t0 -- filtration
+    τ = Time t1 -- stopping rule
+    obsProcess = Proc (Observable Spot_AMZN) - Const 100.0
+    expect = E (disc * Max [ obsProcess * Const 1.0 , aunit ] ) τ f / disc
+
+  -- before expiry
+  value <- fapf observe25 ccy t0 t0 c
+  value === expect
+
+  let
+    obsProcess = Const 25.0 - Const 100.0
+    expect = Max [ obsProcess * Const 1.0 , aunit ]
+
+  -- at expiry (but before exercise)
+  value <- fapf observe25 ccy t1 t0 c
+  value === expect
+
+  pure ()
+
+-- TODO simplify Mul Const 1.0