diff --git a/plutus-ledger-api/changelog.d/20260527_131134_yuriy.lazaryev_issue_2243_fused_unionwith.md b/plutus-ledger-api/changelog.d/20260527_131134_yuriy.lazaryev_issue_2243_fused_unionwith.md
new file mode 100644
index 00000000000..6c21d0f1539
--- /dev/null
+++ b/plutus-ledger-api/changelog.d/20260527_131134_yuriy.lazaryev_issue_2243_fused_unionwith.md
@@ -0,0 +1,3 @@
+### Changed
+
+- Optimised `unionWith` in `PlutusLedgerApi.V1.Data.Value`: same semantics and signature, but the merge now runs in two outer passes instead of three. A constant-factor speedup, not an algorithmic one.
diff --git a/plutus-ledger-api/src/PlutusLedgerApi/V1/Data/Value.hs b/plutus-ledger-api/src/PlutusLedgerApi/V1/Data/Value.hs
index 2d868ac6134..c90e987238b 100644
--- a/plutus-ledger-api/src/PlutusLedgerApi/V1/Data/Value.hs
+++ b/plutus-ledger-api/src/PlutusLedgerApi/V1/Data/Value.hs
@@ -402,31 +402,23 @@ assetClassValueOf :: Value -> AssetClass -> Integer
 assetClassValueOf v (AssetClass (c, t)) = valueOf v c t
 {-# INLINEABLE assetClassValueOf #-}
 
--- | Combine two 'Value' maps, assumes the well-definedness of the two maps.
-unionVal :: Value -> Value -> Map CurrencySymbol (Map TokenName (These Integer Integer))
-unionVal (Value l) (Value r) =
-  let
-    combined = Map.union l r
-    unThese k = case k of
-      This a -> Map.map This a
-      That b -> Map.map That b
-      These a b -> Map.union a b
-   in
-    Map.map unThese combined
-{-# INLINEABLE unionVal #-}
-
 {-| Combine two 'Value' maps with the argument function.
 Assumes the well-definedness of the two maps. -}
 unionWith :: (Integer -> Integer -> Integer) -> Value -> Value -> Value
-unionWith f ls rs =
-  let
-    combined = unionVal ls rs
-    unThese k' = case k' of
+unionWith f (Value mapL) (Value mapR) =
+  Value (Map.map fuseInners (Map.union mapL mapR))
+  where
+    fuseInners :: These (Map TokenName Integer) (Map TokenName Integer) -> Map TokenName Integer
+    fuseInners = \case
+      This innerL -> Map.map (\v -> f v 0) innerL
+      That innerR -> Map.map (\v -> f 0 v) innerR
+      These innerL innerR -> Map.map collapseInner (Map.union innerL innerR)
+
+    collapseInner :: These Integer Integer -> Integer
+    collapseInner = \case
       This a -> f a 0
       That b -> f 0 b
       These a b -> f a b
-   in
-    Value (Map.map (Map.map unThese) combined)
 {-# INLINEABLE unionWith #-}
 
 {-| Convert a 'Value' to a simple list, keeping only the non-zero amounts.
@@ -452,28 +444,26 @@ isZero :: Value -> Bool
 isZero (Value xs) = Map.all (Map.all (\i -> 0 == i)) xs
 {-# INLINEABLE isZero #-}
 
-{-| Checks whether a predicate holds for all the values in a 'Value'
-union. Assumes the well-definedness of the two underlying 'Map's. -}
-checkPred :: (These Integer Integer -> Bool) -> Value -> Value -> Bool
-checkPred f l r =
-  let
-    inner :: Map TokenName (These Integer Integer) -> Bool
-    inner = Map.all f
-   in
-    Map.all inner (unionVal l r)
-{-# INLINEABLE checkPred #-}
-
 {-| Check whether a binary relation holds for value pairs of two 'Value' maps,
-  supplying 0 where a key is only present in one of them. -}
+  supplying 0 where a key is only present in one of them.
+
+Walks the outer 'Map.union' with 'Map.all', short-circuiting on the first pair
+that fails @f@. -}
 checkBinRel :: (Integer -> Integer -> Bool) -> Value -> Value -> Bool
-checkBinRel f l r =
-  let
-    unThese k' = case k' of
+checkBinRel f (Value mapL) (Value mapR) =
+  Map.all checkInners (Map.union mapL mapR)
+  where
+    checkInners :: These (Map TokenName Integer) (Map TokenName Integer) -> Bool
+    checkInners = \case
+      This innerL -> Map.all (\v -> f v 0) innerL
+      That innerR -> Map.all (\v -> f 0 v) innerR
+      These innerL innerR -> Map.all collapseInner (Map.union innerL innerR)
+
+    collapseInner :: These Integer Integer -> Bool
+    collapseInner = \case
       This a -> f a 0
       That b -> f 0 b
       These a b -> f a b
-   in
-    checkPred unThese l r
 {-# INLINEABLE checkBinRel #-}
 
 {-| Check whether one 'Value' is greater than or equal to another. See 'Value' for an explanation
diff --git a/plutus-tx-plugin/test-ledger-api/Spec.hs b/plutus-tx-plugin/test-ledger-api/Spec.hs
index 8b9cd6c4005..b08128679d2 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec.hs
+++ b/plutus-tx-plugin/test-ledger-api/Spec.hs
@@ -28,6 +28,7 @@ tests =
     , Spec.Data.ScriptContext.tests
     , Spec.Data.Value.test_EqValue
     , Spec.Data.Value.test_valueOf
+    , Spec.Data.Value.test_unionWith
     , Spec.Data.MintValue.V3.tests
     , Spec.Envelope.tests
     , Spec.ReturnUnit.V1.tests
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq1.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq1.golden.eval
index 45eb8c5e640..94d5223ca0f 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq1.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq1.golden.eval
@@ -1,6 +1,6 @@
-CPU:               333_462_100
-Memory:                963_345
-AST Size:                  625
-Flat Size:                 942
+CPU:               331_010_215
+Memory:                952_905
+AST Size:                  624
+Flat Size:                 938
 
 (con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq2.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq2.golden.eval
index c8645f0cc91..f42a1ee599d 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq2.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq2.golden.eval
@@ -1,6 +1,6 @@
-CPU:               350_706_346
-Memory:              1_027_715
-AST Size:                  625
-Flat Size:                 993
+CPU:               340_731_162
+Memory:                978_731
+AST Size:                  624
+Flat Size:                 989
 
 (con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq3.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq3.golden.eval
index e7d411ba6d7..36d9ac221bb 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq3.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq3.golden.eval
@@ -1,6 +1,6 @@
-CPU:               363_986_374
-Memory:              1_070_929
-AST Size:                  625
-Flat Size:                 993
+CPU:               351_760_500
+Memory:              1_010_925
+AST Size:                  624
+Flat Size:                 989
 
 (con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq4.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq4.golden.eval
index 99413c67607..f25bce1ac8e 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq4.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq4.golden.eval
@@ -1,6 +1,6 @@
-CPU:               327_778_382
-Memory:                924_936
-AST Size:                  625
-Flat Size:                 949
+CPU:               177_245_560
+Memory:                523_041
+AST Size:                  624
+Flat Size:                 945
 
 (con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq5.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq5.golden.eval
index 8b7b7ebad3e..651a955f076 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq5.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/geq5.golden.eval
@@ -1,6 +1,6 @@
-CPU:               345_381_135
-Memory:                995_200
-AST Size:                  625
-Flat Size:                 949
+CPU:               342_977_250
+Memory:                985_060
+AST Size:                  624
+Flat Size:                 945
 
 (con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt.golden.pir b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt.golden.pir
index 5b7a2eee382..fba8378bbb7 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt.golden.pir
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt.golden.pir
@@ -1,53 +1,9 @@
-letrec
-  !go : list (pair data data) -> bool
-    = \(xs : list (pair data data)) ->
-        case
-          bool
-          xs
-          [ (\(hd : pair data data) ->
-               case
-                 (all dead. list (pair data data) -> bool)
-                 (equalsInteger
-                    0
-                    (unIData (case data hd [(\(l : data) (r : data) -> r)])))
-                 [ (/\dead -> \(ds : list (pair data data)) -> False)
-                 , (/\dead -> go) ]
-                 {all dead. dead})
-          , True ]
-in
 let
-  !`$fToDataInteger_$ctoBuiltinData` : integer -> data
-    = \(i : integer) -> iData i
+  !`$j` : list (pair data data) -> bool = \(ds : list (pair data data)) -> False
   data (These :: * -> * -> *) a b | These_match where
     That : b -> These a b
     These : a -> b -> These a b
     This : a -> These a b
-  !`$fToDataThese_$ctoBuiltinData` :
-     all a b. (\a -> a -> data) a -> (\a -> a -> data) b -> These a b -> data
-    = /\a b ->
-        \(`$dToData` : (\a -> a -> data) a)
-         (`$dToData` : (\a -> a -> data) b)
-         (ds : These a b) ->
-          These_match
-            {a}
-            {b}
-            ds
-            {data}
-            (\(arg : b) -> constrData 1 (mkCons {data} (`$dToData` arg) []))
-            (\(arg : a) (arg : b) ->
-               constrData
-                 2
-                 (mkCons
-                    {data}
-                    (`$dToData` arg)
-                    (mkCons {data} (`$dToData` arg) [])))
-            (\(arg : a) -> constrData 0 (mkCons {data} (`$dToData` arg) []))
-  ~`$dToData` : These integer integer -> data
-    = `$fToDataThese_$ctoBuiltinData`
-        {integer}
-        {integer}
-        `$fToDataInteger_$ctoBuiltinData`
-        `$fToDataInteger_$ctoBuiltinData`
   !`$fUnsafeFromDataThese_$cunsafeFromBuiltinData` :
      all a b. (\a -> data -> a) a -> (\a -> data -> a) b -> data -> These a b
     = /\a b ->
@@ -85,80 +41,67 @@ letrec
           bool
           xs
           [ (\(hd : pair data data) ->
-               case
-                 (all dead. list (pair data data) -> bool)
-                 (let
-                   !k' : These integer integer
-                     = `$fUnsafeFromDataThese_$cunsafeFromBuiltinData`
-                         {integer}
-                         {integer}
-                         unIData
-                         unIData
-                         (case data hd [(\(l : data) (r : data) -> r)])
-                 in
-                 These_match
-                   {integer}
-                   {integer}
-                   k'
-                   {bool}
-                   (\(b : integer) -> lessThanEqualsInteger b 0)
-                   (\(a : integer) (b : integer) -> lessThanEqualsInteger b a)
-                   (\(a : integer) -> lessThanEqualsInteger 0 a))
-                 [ (/\dead -> \(ds : list (pair data data)) -> False)
-                 , (/\dead -> go) ]
-                 {all dead. dead})
-          , True ]
-in
-letrec
-  !go : list (pair data data) -> bool
-    = \(xs : list (pair data data)) ->
-        case
-          bool
-          xs
-          [ (\(hd : pair data data) ->
-               case
-                 (all dead. list (pair data data) -> bool)
-                 (go (unMapData (case data hd [(\(l : data) (r : data) -> r)])))
-                 [ (/\dead -> \(ds : list (pair data data)) -> False)
-                 , (/\dead -> go) ]
-                 {all dead. dead})
+               These_match
+                 {integer}
+                 {integer}
+                 (`$fUnsafeFromDataThese_$cunsafeFromBuiltinData`
+                    {integer}
+                    {integer}
+                    unIData
+                    unIData
+                    (case data hd [(\(l : data) (r : data) -> r)]))
+                 {list (pair data data) -> bool}
+                 (\(b : integer) ->
+                    case
+                      (all dead. list (pair data data) -> bool)
+                      (lessThanEqualsInteger b 0)
+                      [(/\dead -> `$j`), (/\dead -> go)]
+                      {all dead. dead})
+                 (\(a : integer) (b : integer) ->
+                    case
+                      (all dead. list (pair data data) -> bool)
+                      (lessThanEqualsInteger b a)
+                      [(/\dead -> `$j`), (/\dead -> go)]
+                      {all dead. dead})
+                 (\(a : integer) ->
+                    case
+                      (all dead. list (pair data data) -> bool)
+                      (lessThanEqualsInteger 0 a)
+                      [(/\dead -> `$j`), (/\dead -> go)]
+                      {all dead. dead}))
           , True ]
 in
 let
-  !`$fToDataMap_$ctoBuiltinData` :
-     all k a. (\k a -> list (pair data data)) k a -> data
-    = /\k a -> \(ds : (\k a -> list (pair data data)) k a) -> mapData ds
-  !map :
-     all k a b.
+  !`$j` : list (pair data data) -> bool = \(ds : list (pair data data)) -> False
+  !`$fToDataInteger_$ctoBuiltinData` : integer -> data
+    = \(i : integer) -> iData i
+  !all :
+     all k a.
        (\a -> data -> a) a ->
-       (\a -> a -> data) b ->
-       (a -> b) ->
+       (a -> bool) ->
        (\k a -> list (pair data data)) k a ->
-       (\k a -> list (pair data data)) k b
-    = /\k a b ->
-        \(`$dUnsafeFromData` : (\a -> data -> a) a)
-         (`$dToData` : (\a -> a -> data) b)
-         (f : a -> b) ->
+       bool
+    = /\k a ->
+        \(`$dUnsafeFromData` : (\a -> data -> a) a) (p : a -> bool) ->
           letrec
-            !go : list (pair data data) -> list (pair data data)
+            !go : list (pair data data) -> bool
               = \(xs : list (pair data data)) ->
                   case
-                    (list (pair data data))
+                    bool
                     xs
-                    [ (\(hd : pair data data) (eta : list (pair data data)) ->
-                         mkCons
-                           {pair data data}
-                           (mkPairData
-                              (case data hd [(\(l : data) (r : data) -> l)])
-                              (`$dToData`
-                                 (f
-                                    (`$dUnsafeFromData`
-                                       (case
-                                          data
-                                          hd
-                                          [(\(l : data) (r : data) -> r)])))))
-                           (go eta))
-                    , [] ]
+                    [ (\(hd : pair data data) ->
+                         case
+                           (all dead. list (pair data data) -> bool)
+                           (p
+                              (`$dUnsafeFromData`
+                                 (case
+                                    data
+                                    hd
+                                    [(\(l : data) (r : data) -> r)])))
+                           [ (/\dead -> \(ds : list (pair data data)) -> False)
+                           , (/\dead -> go) ]
+                           {all dead. dead})
+                    , True ]
           in
           go
 in
@@ -206,6 +149,26 @@ letrec
           , xs ]
 in
 let
+  !`$fToDataThese_$ctoBuiltinData` :
+     all a b. (\a -> a -> data) a -> (\a -> a -> data) b -> These a b -> data
+    = /\a b ->
+        \(`$dToData` : (\a -> a -> data) a)
+         (`$dToData` : (\a -> a -> data) b)
+         (ds : These a b) ->
+          These_match
+            {a}
+            {b}
+            ds
+            {data}
+            (\(arg : b) -> constrData 1 (mkCons {data} (`$dToData` arg) []))
+            (\(arg : a) (arg : b) ->
+               constrData
+                 2
+                 (mkCons
+                    {data}
+                    (`$dToData` arg)
+                    (mkCons {data} (`$dToData` arg) [])))
+            (\(arg : a) -> constrData 0 (mkCons {data} (`$dToData` arg) []))
   data (Maybe :: * -> *) a | Maybe_match where
     Just : a -> Maybe a
     Nothing : Maybe a
@@ -351,6 +314,72 @@ let
                       , [] ]
             in
             safeAppend (goLeft ds) (goRight ds)
+in
+letrec
+  !go : list (pair data data) -> bool
+    = \(xs : list (pair data data)) ->
+        case
+          bool
+          xs
+          [ (\(hd : pair data data) ->
+               These_match
+                 {(\k a -> list (pair data data)) bytestring integer}
+                 {(\k a -> list (pair data data)) bytestring integer}
+                 (`$fUnsafeFromDataThese_$cunsafeFromBuiltinData`
+                    {(\k a -> list (pair data data)) bytestring integer}
+                    {(\k a -> list (pair data data)) bytestring integer}
+                    (\(eta : data) -> unMapData eta)
+                    (\(eta : data) -> unMapData eta)
+                    (case data hd [(\(l : data) (r : data) -> r)]))
+                 {list (pair data data) -> bool}
+                 (\(innerR :
+                      (\k a -> list (pair data data)) bytestring integer) ->
+                    case
+                      (all dead. list (pair data data) -> bool)
+                      (all
+                         {bytestring}
+                         {integer}
+                         unIData
+                         (\(v : integer) -> lessThanEqualsInteger v 0)
+                         innerR)
+                      [(/\dead -> `$j`), (/\dead -> go)]
+                      {all dead. dead})
+                 (\(innerL : (\k a -> list (pair data data)) bytestring integer)
+                   (innerR :
+                      (\k a -> list (pair data data)) bytestring integer) ->
+                    case
+                      (all dead. list (pair data data) -> bool)
+                      (go
+                         (union
+                            {bytestring}
+                            {integer}
+                            {integer}
+                            unIData
+                            unIData
+                            `$fToDataInteger_$ctoBuiltinData`
+                            `$fToDataInteger_$ctoBuiltinData`
+                            innerL
+                            innerR))
+                      [(/\dead -> `$j`), (/\dead -> go)]
+                      {all dead. dead})
+                 (\(innerL :
+                      (\k a -> list (pair data data)) bytestring integer) ->
+                    case
+                      (all dead. list (pair data data) -> bool)
+                      (all
+                         {bytestring}
+                         {integer}
+                         unIData
+                         (\(v : integer) -> lessThanEqualsInteger 0 v)
+                         innerL)
+                      [(/\dead -> `$j`), (/\dead -> go)]
+                      {all dead. dead}))
+          , True ]
+in
+let
+  !`$fToDataMap_$ctoBuiltinData` :
+     all k a. (\k a -> list (pair data data)) k a -> data
+    = /\k a -> \(ds : (\k a -> list (pair data data)) k a) -> mapData ds
   data Unit | Unit_match where
     Unit : Unit
 in
@@ -580,75 +609,28 @@ in
   case
     (all dead. bool)
     (go
-       (map
+       (union
           {bytestring}
-          {These
-             ((\k a -> list (pair data data)) bytestring integer)
-             ((\k a -> list (pair data data)) bytestring integer)}
-          {(\k a -> list (pair data data)) bytestring (These integer integer)}
-          (`$fUnsafeFromDataThese_$cunsafeFromBuiltinData`
-             {(\k a -> list (pair data data)) bytestring integer}
-             {(\k a -> list (pair data data)) bytestring integer}
-             (\(eta : data) -> unMapData eta)
-             (\(eta : data) -> unMapData eta))
-          (`$fToDataMap_$ctoBuiltinData` {bytestring} {These integer integer})
-          (\(k :
-               These
-                 ((\k a -> list (pair data data)) bytestring integer)
-                 ((\k a -> list (pair data data)) bytestring integer)) ->
-             These_match
-               {(\k a -> list (pair data data)) bytestring integer}
-               {(\k a -> list (pair data data)) bytestring integer}
-               k
-               {(\k a -> list (pair data data))
-                  bytestring
-                  (These integer integer)}
-               (\(b : (\k a -> list (pair data data)) bytestring integer) ->
-                  map
-                    {bytestring}
-                    {integer}
-                    {These integer integer}
-                    unIData
-                    `$dToData`
-                    (\(ds : integer) -> That {integer} {integer} ds)
-                    b)
-               (\(a : (\k a -> list (pair data data)) bytestring integer)
-                 (b : (\k a -> list (pair data data)) bytestring integer) ->
-                  union
-                    {bytestring}
-                    {integer}
-                    {integer}
-                    unIData
-                    unIData
-                    `$fToDataInteger_$ctoBuiltinData`
-                    `$fToDataInteger_$ctoBuiltinData`
-                    a
-                    b)
-               (\(a : (\k a -> list (pair data data)) bytestring integer) ->
-                  map
-                    {bytestring}
-                    {integer}
-                    {These integer integer}
-                    unIData
-                    `$dToData`
-                    (\(ds : integer) -> This {integer} {integer} ds)
-                    a))
-          (union
-             {bytestring}
-             {(\k a -> list (pair data data)) bytestring integer}
-             {(\k a -> list (pair data data)) bytestring integer}
-             (\(eta : data) -> unMapData eta)
-             (\(eta : data) -> unMapData eta)
-             (`$fToDataMap_$ctoBuiltinData` {bytestring} {integer})
-             (`$fToDataMap_$ctoBuiltinData` {bytestring} {integer})
-             l
-             r)))
+          {(\k a -> list (pair data data)) bytestring integer}
+          {(\k a -> list (pair data data)) bytestring integer}
+          (\(eta : data) -> unMapData eta)
+          (\(eta : data) -> unMapData eta)
+          (`$fToDataMap_$ctoBuiltinData` {bytestring} {integer})
+          (`$fToDataMap_$ctoBuiltinData` {bytestring} {integer})
+          l
+          r))
     [ (/\dead -> False)
     , (/\dead ->
          case
            bool
            (unordEqWith
-              (\(v : data) -> go (unMapData v))
+              (\(v : data) ->
+                 all
+                   {bytestring}
+                   {integer}
+                   unIData
+                   (\(v : integer) -> equalsInteger 0 v)
+                   (unMapData v))
               (\(v : data) (v : data) ->
                  unordEqWith
                    (\(v : data) -> equalsInteger 0 (unIData v))
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt1.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt1.golden.eval
index 78b538a086f..42c192516e1 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt1.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt1.golden.eval
@@ -1,6 +1,6 @@
-CPU:               384_062_505
-Memory:              1_141_260
-AST Size:                1_006
-Flat Size:               1_316
+CPU:               381_466_620
+Memory:              1_129_920
+AST Size:                  980
+Flat Size:               1_291
 
 (con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt2.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt2.golden.eval
index 7739a9714ce..018f987a5f4 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt2.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt2.golden.eval
@@ -1,6 +1,6 @@
-CPU:               351_074_346
-Memory:              1_030_015
-AST Size:                1_006
-Flat Size:               1_367
+CPU:               340_955_162
+Memory:                980_131
+AST Size:                  980
+Flat Size:               1_342
 
 (con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt3.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt3.golden.eval
index efe0e10e62d..8ef5b85fae8 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt3.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt3.golden.eval
@@ -1,6 +1,6 @@
-CPU:               415_308_479
-Memory:              1_252_809
-AST Size:                1_006
-Flat Size:               1_367
+CPU:               403_162_605
+Memory:              1_193_305
+AST Size:                  980
+Flat Size:               1_342
 
 (con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt4.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt4.golden.eval
index f03788378df..1d31f796d4a 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt4.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt4.golden.eval
@@ -1,6 +1,6 @@
-CPU:               328_146_382
-Memory:                927_236
-AST Size:                1_006
-Flat Size:               1_323
+CPU:               177_469_560
+Memory:                524_441
+AST Size:                  980
+Flat Size:               1_298
 
 (con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt5.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt5.golden.eval
index a26a16efbbd..035f33d2aad 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt5.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.12/gt5.golden.eval
@@ -1,6 +1,6 @@
-CPU:               369_587_763
-Memory:              1_084_024
-AST Size:                1_006
-Flat Size:               1_323
+CPU:               367_039_878
+Memory:              1_072_984
+AST Size:                  980
+Flat Size:               1_298
 
 (con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq1.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq1.golden.eval
index 45eb8c5e640..94d5223ca0f 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq1.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq1.golden.eval
@@ -1,6 +1,6 @@
-CPU:               333_462_100
-Memory:                963_345
-AST Size:                  625
-Flat Size:                 942
+CPU:               331_010_215
+Memory:                952_905
+AST Size:                  624
+Flat Size:                 938
 
 (con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq2.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq2.golden.eval
index c8645f0cc91..f42a1ee599d 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq2.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq2.golden.eval
@@ -1,6 +1,6 @@
-CPU:               350_706_346
-Memory:              1_027_715
-AST Size:                  625
-Flat Size:                 993
+CPU:               340_731_162
+Memory:                978_731
+AST Size:                  624
+Flat Size:                 989
 
 (con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq3.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq3.golden.eval
index e7d411ba6d7..36d9ac221bb 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq3.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq3.golden.eval
@@ -1,6 +1,6 @@
-CPU:               363_986_374
-Memory:              1_070_929
-AST Size:                  625
-Flat Size:                 993
+CPU:               351_760_500
+Memory:              1_010_925
+AST Size:                  624
+Flat Size:                 989
 
 (con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq4.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq4.golden.eval
index 99413c67607..f25bce1ac8e 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq4.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq4.golden.eval
@@ -1,6 +1,6 @@
-CPU:               327_778_382
-Memory:                924_936
-AST Size:                  625
-Flat Size:                 949
+CPU:               177_245_560
+Memory:                523_041
+AST Size:                  624
+Flat Size:                 945
 
 (con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq5.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq5.golden.eval
index 8b7b7ebad3e..651a955f076 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq5.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/geq5.golden.eval
@@ -1,6 +1,6 @@
-CPU:               345_381_135
-Memory:                995_200
-AST Size:                  625
-Flat Size:                 949
+CPU:               342_977_250
+Memory:                985_060
+AST Size:                  624
+Flat Size:                 945
 
 (con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt.golden.pir b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt.golden.pir
index 5b7a2eee382..fba8378bbb7 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt.golden.pir
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt.golden.pir
@@ -1,53 +1,9 @@
-letrec
-  !go : list (pair data data) -> bool
-    = \(xs : list (pair data data)) ->
-        case
-          bool
-          xs
-          [ (\(hd : pair data data) ->
-               case
-                 (all dead. list (pair data data) -> bool)
-                 (equalsInteger
-                    0
-                    (unIData (case data hd [(\(l : data) (r : data) -> r)])))
-                 [ (/\dead -> \(ds : list (pair data data)) -> False)
-                 , (/\dead -> go) ]
-                 {all dead. dead})
-          , True ]
-in
 let
-  !`$fToDataInteger_$ctoBuiltinData` : integer -> data
-    = \(i : integer) -> iData i
+  !`$j` : list (pair data data) -> bool = \(ds : list (pair data data)) -> False
   data (These :: * -> * -> *) a b | These_match where
     That : b -> These a b
     These : a -> b -> These a b
     This : a -> These a b
-  !`$fToDataThese_$ctoBuiltinData` :
-     all a b. (\a -> a -> data) a -> (\a -> a -> data) b -> These a b -> data
-    = /\a b ->
-        \(`$dToData` : (\a -> a -> data) a)
-         (`$dToData` : (\a -> a -> data) b)
-         (ds : These a b) ->
-          These_match
-            {a}
-            {b}
-            ds
-            {data}
-            (\(arg : b) -> constrData 1 (mkCons {data} (`$dToData` arg) []))
-            (\(arg : a) (arg : b) ->
-               constrData
-                 2
-                 (mkCons
-                    {data}
-                    (`$dToData` arg)
-                    (mkCons {data} (`$dToData` arg) [])))
-            (\(arg : a) -> constrData 0 (mkCons {data} (`$dToData` arg) []))
-  ~`$dToData` : These integer integer -> data
-    = `$fToDataThese_$ctoBuiltinData`
-        {integer}
-        {integer}
-        `$fToDataInteger_$ctoBuiltinData`
-        `$fToDataInteger_$ctoBuiltinData`
   !`$fUnsafeFromDataThese_$cunsafeFromBuiltinData` :
      all a b. (\a -> data -> a) a -> (\a -> data -> a) b -> data -> These a b
     = /\a b ->
@@ -85,80 +41,67 @@ letrec
           bool
           xs
           [ (\(hd : pair data data) ->
-               case
-                 (all dead. list (pair data data) -> bool)
-                 (let
-                   !k' : These integer integer
-                     = `$fUnsafeFromDataThese_$cunsafeFromBuiltinData`
-                         {integer}
-                         {integer}
-                         unIData
-                         unIData
-                         (case data hd [(\(l : data) (r : data) -> r)])
-                 in
-                 These_match
-                   {integer}
-                   {integer}
-                   k'
-                   {bool}
-                   (\(b : integer) -> lessThanEqualsInteger b 0)
-                   (\(a : integer) (b : integer) -> lessThanEqualsInteger b a)
-                   (\(a : integer) -> lessThanEqualsInteger 0 a))
-                 [ (/\dead -> \(ds : list (pair data data)) -> False)
-                 , (/\dead -> go) ]
-                 {all dead. dead})
-          , True ]
-in
-letrec
-  !go : list (pair data data) -> bool
-    = \(xs : list (pair data data)) ->
-        case
-          bool
-          xs
-          [ (\(hd : pair data data) ->
-               case
-                 (all dead. list (pair data data) -> bool)
-                 (go (unMapData (case data hd [(\(l : data) (r : data) -> r)])))
-                 [ (/\dead -> \(ds : list (pair data data)) -> False)
-                 , (/\dead -> go) ]
-                 {all dead. dead})
+               These_match
+                 {integer}
+                 {integer}
+                 (`$fUnsafeFromDataThese_$cunsafeFromBuiltinData`
+                    {integer}
+                    {integer}
+                    unIData
+                    unIData
+                    (case data hd [(\(l : data) (r : data) -> r)]))
+                 {list (pair data data) -> bool}
+                 (\(b : integer) ->
+                    case
+                      (all dead. list (pair data data) -> bool)
+                      (lessThanEqualsInteger b 0)
+                      [(/\dead -> `$j`), (/\dead -> go)]
+                      {all dead. dead})
+                 (\(a : integer) (b : integer) ->
+                    case
+                      (all dead. list (pair data data) -> bool)
+                      (lessThanEqualsInteger b a)
+                      [(/\dead -> `$j`), (/\dead -> go)]
+                      {all dead. dead})
+                 (\(a : integer) ->
+                    case
+                      (all dead. list (pair data data) -> bool)
+                      (lessThanEqualsInteger 0 a)
+                      [(/\dead -> `$j`), (/\dead -> go)]
+                      {all dead. dead}))
           , True ]
 in
 let
-  !`$fToDataMap_$ctoBuiltinData` :
-     all k a. (\k a -> list (pair data data)) k a -> data
-    = /\k a -> \(ds : (\k a -> list (pair data data)) k a) -> mapData ds
-  !map :
-     all k a b.
+  !`$j` : list (pair data data) -> bool = \(ds : list (pair data data)) -> False
+  !`$fToDataInteger_$ctoBuiltinData` : integer -> data
+    = \(i : integer) -> iData i
+  !all :
+     all k a.
        (\a -> data -> a) a ->
-       (\a -> a -> data) b ->
-       (a -> b) ->
+       (a -> bool) ->
        (\k a -> list (pair data data)) k a ->
-       (\k a -> list (pair data data)) k b
-    = /\k a b ->
-        \(`$dUnsafeFromData` : (\a -> data -> a) a)
-         (`$dToData` : (\a -> a -> data) b)
-         (f : a -> b) ->
+       bool
+    = /\k a ->
+        \(`$dUnsafeFromData` : (\a -> data -> a) a) (p : a -> bool) ->
           letrec
-            !go : list (pair data data) -> list (pair data data)
+            !go : list (pair data data) -> bool
               = \(xs : list (pair data data)) ->
                   case
-                    (list (pair data data))
+                    bool
                     xs
-                    [ (\(hd : pair data data) (eta : list (pair data data)) ->
-                         mkCons
-                           {pair data data}
-                           (mkPairData
-                              (case data hd [(\(l : data) (r : data) -> l)])
-                              (`$dToData`
-                                 (f
-                                    (`$dUnsafeFromData`
-                                       (case
-                                          data
-                                          hd
-                                          [(\(l : data) (r : data) -> r)])))))
-                           (go eta))
-                    , [] ]
+                    [ (\(hd : pair data data) ->
+                         case
+                           (all dead. list (pair data data) -> bool)
+                           (p
+                              (`$dUnsafeFromData`
+                                 (case
+                                    data
+                                    hd
+                                    [(\(l : data) (r : data) -> r)])))
+                           [ (/\dead -> \(ds : list (pair data data)) -> False)
+                           , (/\dead -> go) ]
+                           {all dead. dead})
+                    , True ]
           in
           go
 in
@@ -206,6 +149,26 @@ letrec
           , xs ]
 in
 let
+  !`$fToDataThese_$ctoBuiltinData` :
+     all a b. (\a -> a -> data) a -> (\a -> a -> data) b -> These a b -> data
+    = /\a b ->
+        \(`$dToData` : (\a -> a -> data) a)
+         (`$dToData` : (\a -> a -> data) b)
+         (ds : These a b) ->
+          These_match
+            {a}
+            {b}
+            ds
+            {data}
+            (\(arg : b) -> constrData 1 (mkCons {data} (`$dToData` arg) []))
+            (\(arg : a) (arg : b) ->
+               constrData
+                 2
+                 (mkCons
+                    {data}
+                    (`$dToData` arg)
+                    (mkCons {data} (`$dToData` arg) [])))
+            (\(arg : a) -> constrData 0 (mkCons {data} (`$dToData` arg) []))
   data (Maybe :: * -> *) a | Maybe_match where
     Just : a -> Maybe a
     Nothing : Maybe a
@@ -351,6 +314,72 @@ let
                       , [] ]
             in
             safeAppend (goLeft ds) (goRight ds)
+in
+letrec
+  !go : list (pair data data) -> bool
+    = \(xs : list (pair data data)) ->
+        case
+          bool
+          xs
+          [ (\(hd : pair data data) ->
+               These_match
+                 {(\k a -> list (pair data data)) bytestring integer}
+                 {(\k a -> list (pair data data)) bytestring integer}
+                 (`$fUnsafeFromDataThese_$cunsafeFromBuiltinData`
+                    {(\k a -> list (pair data data)) bytestring integer}
+                    {(\k a -> list (pair data data)) bytestring integer}
+                    (\(eta : data) -> unMapData eta)
+                    (\(eta : data) -> unMapData eta)
+                    (case data hd [(\(l : data) (r : data) -> r)]))
+                 {list (pair data data) -> bool}
+                 (\(innerR :
+                      (\k a -> list (pair data data)) bytestring integer) ->
+                    case
+                      (all dead. list (pair data data) -> bool)
+                      (all
+                         {bytestring}
+                         {integer}
+                         unIData
+                         (\(v : integer) -> lessThanEqualsInteger v 0)
+                         innerR)
+                      [(/\dead -> `$j`), (/\dead -> go)]
+                      {all dead. dead})
+                 (\(innerL : (\k a -> list (pair data data)) bytestring integer)
+                   (innerR :
+                      (\k a -> list (pair data data)) bytestring integer) ->
+                    case
+                      (all dead. list (pair data data) -> bool)
+                      (go
+                         (union
+                            {bytestring}
+                            {integer}
+                            {integer}
+                            unIData
+                            unIData
+                            `$fToDataInteger_$ctoBuiltinData`
+                            `$fToDataInteger_$ctoBuiltinData`
+                            innerL
+                            innerR))
+                      [(/\dead -> `$j`), (/\dead -> go)]
+                      {all dead. dead})
+                 (\(innerL :
+                      (\k a -> list (pair data data)) bytestring integer) ->
+                    case
+                      (all dead. list (pair data data) -> bool)
+                      (all
+                         {bytestring}
+                         {integer}
+                         unIData
+                         (\(v : integer) -> lessThanEqualsInteger 0 v)
+                         innerL)
+                      [(/\dead -> `$j`), (/\dead -> go)]
+                      {all dead. dead}))
+          , True ]
+in
+let
+  !`$fToDataMap_$ctoBuiltinData` :
+     all k a. (\k a -> list (pair data data)) k a -> data
+    = /\k a -> \(ds : (\k a -> list (pair data data)) k a) -> mapData ds
   data Unit | Unit_match where
     Unit : Unit
 in
@@ -580,75 +609,28 @@ in
   case
     (all dead. bool)
     (go
-       (map
+       (union
           {bytestring}
-          {These
-             ((\k a -> list (pair data data)) bytestring integer)
-             ((\k a -> list (pair data data)) bytestring integer)}
-          {(\k a -> list (pair data data)) bytestring (These integer integer)}
-          (`$fUnsafeFromDataThese_$cunsafeFromBuiltinData`
-             {(\k a -> list (pair data data)) bytestring integer}
-             {(\k a -> list (pair data data)) bytestring integer}
-             (\(eta : data) -> unMapData eta)
-             (\(eta : data) -> unMapData eta))
-          (`$fToDataMap_$ctoBuiltinData` {bytestring} {These integer integer})
-          (\(k :
-               These
-                 ((\k a -> list (pair data data)) bytestring integer)
-                 ((\k a -> list (pair data data)) bytestring integer)) ->
-             These_match
-               {(\k a -> list (pair data data)) bytestring integer}
-               {(\k a -> list (pair data data)) bytestring integer}
-               k
-               {(\k a -> list (pair data data))
-                  bytestring
-                  (These integer integer)}
-               (\(b : (\k a -> list (pair data data)) bytestring integer) ->
-                  map
-                    {bytestring}
-                    {integer}
-                    {These integer integer}
-                    unIData
-                    `$dToData`
-                    (\(ds : integer) -> That {integer} {integer} ds)
-                    b)
-               (\(a : (\k a -> list (pair data data)) bytestring integer)
-                 (b : (\k a -> list (pair data data)) bytestring integer) ->
-                  union
-                    {bytestring}
-                    {integer}
-                    {integer}
-                    unIData
-                    unIData
-                    `$fToDataInteger_$ctoBuiltinData`
-                    `$fToDataInteger_$ctoBuiltinData`
-                    a
-                    b)
-               (\(a : (\k a -> list (pair data data)) bytestring integer) ->
-                  map
-                    {bytestring}
-                    {integer}
-                    {These integer integer}
-                    unIData
-                    `$dToData`
-                    (\(ds : integer) -> This {integer} {integer} ds)
-                    a))
-          (union
-             {bytestring}
-             {(\k a -> list (pair data data)) bytestring integer}
-             {(\k a -> list (pair data data)) bytestring integer}
-             (\(eta : data) -> unMapData eta)
-             (\(eta : data) -> unMapData eta)
-             (`$fToDataMap_$ctoBuiltinData` {bytestring} {integer})
-             (`$fToDataMap_$ctoBuiltinData` {bytestring} {integer})
-             l
-             r)))
+          {(\k a -> list (pair data data)) bytestring integer}
+          {(\k a -> list (pair data data)) bytestring integer}
+          (\(eta : data) -> unMapData eta)
+          (\(eta : data) -> unMapData eta)
+          (`$fToDataMap_$ctoBuiltinData` {bytestring} {integer})
+          (`$fToDataMap_$ctoBuiltinData` {bytestring} {integer})
+          l
+          r))
     [ (/\dead -> False)
     , (/\dead ->
          case
            bool
            (unordEqWith
-              (\(v : data) -> go (unMapData v))
+              (\(v : data) ->
+                 all
+                   {bytestring}
+                   {integer}
+                   unIData
+                   (\(v : integer) -> equalsInteger 0 v)
+                   (unMapData v))
               (\(v : data) (v : data) ->
                  unordEqWith
                    (\(v : data) -> equalsInteger 0 (unIData v))
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt1.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt1.golden.eval
index 78b538a086f..42c192516e1 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt1.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt1.golden.eval
@@ -1,6 +1,6 @@
-CPU:               384_062_505
-Memory:              1_141_260
-AST Size:                1_006
-Flat Size:               1_316
+CPU:               381_466_620
+Memory:              1_129_920
+AST Size:                  980
+Flat Size:               1_291
 
 (con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt2.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt2.golden.eval
index 7739a9714ce..018f987a5f4 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt2.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt2.golden.eval
@@ -1,6 +1,6 @@
-CPU:               351_074_346
-Memory:              1_030_015
-AST Size:                1_006
-Flat Size:               1_367
+CPU:               340_955_162
+Memory:                980_131
+AST Size:                  980
+Flat Size:               1_342
 
 (con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt3.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt3.golden.eval
index efe0e10e62d..8ef5b85fae8 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt3.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt3.golden.eval
@@ -1,6 +1,6 @@
-CPU:               415_308_479
-Memory:              1_252_809
-AST Size:                1_006
-Flat Size:               1_367
+CPU:               403_162_605
+Memory:              1_193_305
+AST Size:                  980
+Flat Size:               1_342
 
 (con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt4.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt4.golden.eval
index f03788378df..1d31f796d4a 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt4.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt4.golden.eval
@@ -1,6 +1,6 @@
-CPU:               328_146_382
-Memory:                927_236
-AST Size:                1_006
-Flat Size:               1_323
+CPU:               177_469_560
+Memory:                524_441
+AST Size:                  980
+Flat Size:               1_298
 
 (con bool False)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt5.golden.eval b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt5.golden.eval
index a26a16efbbd..035f33d2aad 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt5.golden.eval
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Budget/9.6/gt5.golden.eval
@@ -1,6 +1,6 @@
-CPU:               369_587_763
-Memory:              1_084_024
-AST Size:                1_006
-Flat Size:               1_323
+CPU:               367_039_878
+Memory:              1_072_984
+AST Size:                  980
+Flat Size:               1_298
 
 (con bool True)
\ No newline at end of file
diff --git a/plutus-tx-plugin/test-ledger-api/Spec/Data/Value.hs b/plutus-tx-plugin/test-ledger-api/Spec/Data/Value.hs
index 3b321e3c516..b47612adfe3 100644
--- a/plutus-tx-plugin/test-ledger-api/Spec/Data/Value.hs
+++ b/plutus-tx-plugin/test-ledger-api/Spec/Data/Value.hs
@@ -318,3 +318,62 @@ test_valueOf =
                   `unsafeApplyCode` liftCodeDef (unCurrencySymbol cs)
                   `unsafeApplyCode` liftCodeDef (unTokenName tn)
            in nonBuiltin === builtin
+
+{-| The 'unionWith' @(+)@ under test. Signature matches 'compiledBuiltinUnion' so the property
+can pit them against each other. -}
+compiledUnionWith :: CompiledCode (BI.BuiltinData -> BI.BuiltinData -> BI.BuiltinData)
+compiledUnionWith = plinthc \bd1 bd2 ->
+  Tx.toBuiltinData (unionWith (+) (Tx.unsafeFromBuiltinData bd1) (Tx.unsafeFromBuiltinData bd2))
+
+{-| Independent oracle: the builtin union path. Shares no source with 'compiledUnionWith', so a
+bug in one cannot hide behind the same bug in the other. -}
+compiledBuiltinUnion :: CompiledCode (BI.BuiltinData -> BI.BuiltinData -> BI.BuiltinData)
+compiledBuiltinUnion = plinthc \bd1 bd2 ->
+  B.mkValue (B.unionValue (B.unsafeDataAsValue bd1) (B.unsafeDataAsValue bd2))
+
+-- | Evaluate a compiled union on CEK and decode its result.
+runUnionCode
+  :: CompiledCode (BI.BuiltinData -> BI.BuiltinData -> BI.BuiltinData)
+  -> Value
+  -> Value
+  -> Value
+runUnionCode code value1 value2 =
+  Tx.unsafeFromBuiltinData
+    . BI.dataToBuiltinData
+    . either Haskell.throw id
+    $ errOrRes
+    >>= PLC.readKnownSelf
+  where
+    prog =
+      code
+        `unsafeApplyCode` liftCodeDef (Tx.toBuiltinData value1)
+        `unsafeApplyCode` liftCodeDef (Tx.toBuiltinData value2)
+    (errOrRes, _cost) =
+      PLC.runCekNoEmit PLC.defaultCekParametersForTesting PLC.counting
+        . PLC.runQuote
+        . PLC.unDeBruijnTermWith (Haskell.error "Free variable")
+        . PLC._progTerm
+        $ getPlc prog
+
+-- | 'unionWith' @(+)@ must agree with the builtin union path on CEK.
+test_unionWith :: TestTree
+test_unionWith =
+  testProperty "non-builtin unionWith matches builtin unionValue on CEK" \rawValue1 rawValue2 ->
+    let v1 = normalise rawValue1
+        v2 = normalise rawValue2
+        -- Compare semantically: key order and zero-sum entries differ between the paths but
+        -- carry no meaning, so canonicalise before '==='.
+        canon code = normaliseLists . valueToLists $ runUnionCode code v1 v2
+     in canon compiledUnionWith === canon compiledBuiltinUnion
+
+{-| Restrict an arbitrary 'Value' to the well-formed domain 'unsafeDataAsValue' accepts: the
+builtin errors on unsorted keys, zero quantities, or empty token maps. -}
+normaliseLists
+  :: [(CurrencySymbol, [(TokenName, Integer)])] -> [(CurrencySymbol, [(TokenName, Integer)])]
+normaliseLists =
+  Haskell.sortOn fst
+    . Haskell.filter (Haskell.not . Haskell.null . snd)
+    . Haskell.map (Haskell.fmap (Haskell.sortOn fst . Haskell.filter ((Haskell./= 0) . snd)))
+
+normalise :: Value -> Value
+normalise = listsToValue . normaliseLists . valueToLists