diff --git a/spectec/src/al/free.mli b/spectec/src/al/free.mli
index 9f9e58bafd..9c124b1c9d 100644
--- a/spectec/src/al/free.mli
+++ b/spectec/src/al/free.mli
@@ -2,5 +2,6 @@ open Ast
 
 module IdSet : Set.S with type elt = string
 
+val free_list : ('a -> IdSet.t) -> 'a list -> IdSet.t
 val free_expr : expr -> IdSet.t
 val free_instr : instr -> IdSet.t
diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml
index 668e3ebd7f..a1e9455d19 100644
--- a/spectec/src/il2al/translate.ml
+++ b/spectec/src/il2al/translate.ml
@@ -468,14 +468,10 @@ let contains_diff target_ns e =
   not (IdSet.is_empty free_ns) && IdSet.disjoint free_ns target_ns
 
 let extract_diff lhs rhs ids cont =
-  let at = lhs.at in
   match lhs.it with
   (* TODO: Make this actually consider the targets *)
-  | CallE (f, args) ->
-    let hds, tl = Util.Lib.List.split_last args in
-    let new_lhs = tl in
-    let new_rhs = callE ("inverse_of_" ^ f, hds @ [ rhs ]) ~at:at in
-    new_lhs, new_rhs, cont
+  | CallE (_, _) ->
+    lhs, rhs, cont
   | _ ->
     let conds = ref [] in
     let target_ns = IdSet.of_list (List.map it ids) in
@@ -484,7 +480,7 @@ let extract_diff lhs rhs ids cont =
         e
       else
         let new_e = get_lhs_name () in
-        conds := !conds @ [ binE (EqOp, new_e, e) ];
+        conds := [ binE (EqOp, new_e, e) ];
         new_e
     ) in
     let walker = Al.Walk.walk_expr { Al.Walk.default_config with
@@ -502,31 +498,70 @@ let rec translate_bindings ids cont bindings =
     | _ -> translate_letpr l r ids cont
   ) bindings cont
 
+and translate_letpr lhs rhs free_ids cont =
+  (* helpers *)
+  let contains_free expr =
+    free_ids
+    |> List.map it
+    |> IdSet.of_list
+    |> IdSet.disjoint (free_expr expr)
+    |> not
+  in
+  let rhs2args e =
+    match e.it with
+    | TupE el -> el
+    | _ -> [e]
+  in
+  let args2lhs args = if List.length args = 1 then List.hd args else tupE args in
 
-and translate_letpr lhs rhs ids cont =
-  let lhs, rhs, cont = extract_diff lhs rhs ids cont in
-  let lhs_at = lhs.at in
-  let rhs_at = rhs.at in
-  let at = over_region [ lhs_at; rhs_at ] in
+  let lhs, rhs, cont = extract_diff lhs rhs free_ids cont in
+  let at = over_region [ lhs.at; rhs.at ] in
   match lhs.it with
+  | CallE (f, args) when List.for_all contains_free args ->
+    let new_lhs = args2lhs args in
+    let new_rhs = InvCallE (f, [], rhs2args rhs) $ lhs.at in
+    translate_letpr new_lhs new_rhs free_ids cont
+  | CallE (f, args) when List.exists contains_free args ->
+    (* Distinguish free arguments and bound arguments *)
+    let free_args_with_index, bound_args =
+      args
+      |> List.mapi (fun i arg ->
+          if contains_free arg then Some (arg, i), None
+          else None, Some arg
+        )
+      |> List.split
+    in
+    let bound_args = List.filter_map (fun x -> x) bound_args in
+    let free_args, indices =
+      free_args_with_index
+      |> List.filter_map (fun x -> x)
+      |> List.split
+    in
+
+    (* Free argument become new lhs & InvCallE become new rhs *)
+    let new_lhs = args2lhs free_args in
+    let new_rhs = InvCallE (f, indices, bound_args @ rhs2args rhs) $ lhs.at in
+
+    (* Recursively translate new_lhs and new_rhs *)
+    translate_letpr new_lhs new_rhs free_ids cont
   | CaseE (tag, es) ->
     let bindings, es' = extract_non_names es in
     [
       ifI (
         isCaseOfE (rhs, tag),
-        letI (caseE (tag, es') ~at:lhs_at, rhs) ~at:at :: translate_bindings ids cont bindings,
+        letI (caseE (tag, es') ~at:lhs.at, rhs) ~at:at :: translate_bindings free_ids cont bindings,
         []
       );
     ]
   | ListE es ->
     let bindings, es' = extract_non_names es in
     if List.length es >= 2 then (* TODO: remove this. This is temporarily for a pure function returning stores *)
-    letI (listE es' ~at:lhs_at, rhs) ~at:at :: translate_bindings ids cont bindings
+    letI (listE es' ~at:lhs.at, rhs) ~at:at :: translate_bindings free_ids cont bindings
     else
     [
       ifI
         ( binE (EqOp, lenE rhs, numE (Z.of_int (List.length es))),
-          letI (listE es' ~at:lhs_at, rhs) ~at:at :: translate_bindings ids cont bindings,
+          letI (listE es' ~at:lhs.at, rhs) ~at:at :: translate_bindings free_ids cont bindings,
           [] );
     ]
   | OptE None ->
@@ -548,7 +583,7 @@ and translate_letpr lhs rhs ids cont =
     [
       ifI
         ( isDefinedE rhs,
-          letI (optE (Some fresh) ~at:lhs_at, rhs) ~at:at :: translate_letpr e fresh ids cont,
+          letI (optE (Some fresh) ~at:lhs.at, rhs) ~at:at :: translate_letpr e fresh free_ids cont,
           [] );
      ]
   | BinE (AddOp, a, b) ->
@@ -580,15 +615,15 @@ and translate_letpr lhs rhs ids cont =
     [
       ifI
         ( cond,
-          letI (catE (prefix', suffix') ~at:lhs_at, rhs) ~at:at
-            :: translate_bindings ids cont (bindings_p @ bindings_s),
+          letI (catE (prefix', suffix') ~at:lhs.at, rhs) ~at:at
+            :: translate_bindings free_ids cont (bindings_p @ bindings_s),
           [] );
     ]
   | SubE (s, t) ->
     [
       ifI
         ( hasTypeE (rhs, t),
-          letI (varE s ~at:lhs_at, rhs) ~at:at :: cont,
+          letI (varE s ~at:lhs.at, rhs) ~at:at :: cont,
           [] )
     ]
   | _ -> letI (lhs, rhs) ~at:at :: cont
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
index 61b1a8947d..17c9682c3c 100644
--- a/spectec/test-prose/TEST.md
+++ b/spectec/test-prose/TEST.md
@@ -285,7 +285,7 @@ signed N i
 4. Return (i - (2 ^ N)).
 
 invsigned N ii
-1. Let j be $inverse_of_signed(N, ii).
+1. Let j be $signed_1^-1(N, ii).
 2. Return j.
 
 unop valty_u1 unop__u0 val__u3
@@ -541,11 +541,11 @@ cvtop valty_u0 valty_u1 cvtop_u2 val__u4
 15. Return [$reinterpret(Fnn, Inn, fN)].
 
 invibytes N b*
-1. Let n be $inverse_of_ibytes(N, b*).
+1. Let n be $ibytes_1^-1(N, b*).
 2. Return n.
 
 invfbytes N b*
-1. Let p be $inverse_of_fbytes(N, b*).
+1. Let p be $fbytes_1^-1(N, b*).
 2. Return p.
 
 default_ valty_u0
@@ -1105,7 +1105,7 @@ execution_of_LOAD valty_u0 sz_sx_u1? ao
   a. Let t be valty_u0.
   b. If (((i + ao.OFFSET) + ($size(t) / 8)) > |$mem(z, 0).BYTES|), then:
     1) Trap.
-  c. Let c be $inverse_of_bytes(t, $mem(z, 0).BYTES[(i + ao.OFFSET) : ($size(t) / 8)]).
+  c. Let c be $bytes_1^-1(t, $mem(z, 0).BYTES[(i + ao.OFFSET) : ($size(t) / 8)]).
   d. Push the value (t.CONST c) to the stack.
 5. If the type of valty_u0 is Inn, then:
   a. If sz_sx_u1? is defined, then:
@@ -1117,7 +1117,7 @@ execution_of_LOAD valty_u0 sz_sx_u1? ao
   c. If sz_sx_u1? is defined, then:
     1) Let ?(y_0) be sz_sx_u1?.
     2) Let (n, sx) be y_0.
-    3) Let c be $inverse_of_ibytes(n, $mem(z, 0).BYTES[(i + ao.OFFSET) : (n / 8)]).
+    3) Let c be $ibytes_1^-1(n, $mem(z, 0).BYTES[(i + ao.OFFSET) : (n / 8)]).
     4) Push the value (Inn.CONST $ext(n, $size(Inn), sx, c)) to the stack.
 
 execution_of_MEMORY.SIZE
@@ -1738,7 +1738,7 @@ signed N i
 4. Return (i - (2 ^ N)).
 
 invsigned N i
-1. Let j be $inverse_of_signed(N, i).
+1. Let j be $signed_1^-1(N, i).
 2. Return j.
 
 unop numty_u1 unop__u0 num__u3
@@ -2003,11 +2003,11 @@ cvtop numty_u0 numty_u1 cvtop_u2 num__u4
 15. Return [$reinterpret(Fnn, Inn, fN)].
 
 invibytes N b*
-1. Let n be $inverse_of_ibytes(N, b*).
+1. Let n be $ibytes_1^-1(N, b*).
 2. Return n.
 
 invfbytes N b*
-1. Let p be $inverse_of_fbytes(N, b*).
+1. Let p be $fbytes_1^-1(N, b*).
 2. Return p.
 
 packnum lanet_u0 c
@@ -2025,7 +2025,7 @@ unpacknum lanet_u0 c
 4. Return $ext($psize(packtype), $size($unpack(packtype)), U, c).
 
 invlanes_ sh c*
-1. Let vc be $inverse_of_lanes_(sh, c*).
+1. Let vc be $lanes__1^-1(sh, c*).
 2. Return vc.
 
 halfop half_u0 i j
@@ -2259,7 +2259,7 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
   a. Let Fnn be lanet_u1.
   b. Let lane_1* be $lanes_((Fnn X N), v128_1).
   c. Let lane_2* be $lanes_((Fnn X N), v128_2).
-  d. Let Inn be $inverse_of_isize($size(Fnn)).
+  d. Let Inn be $isize^-1($size(Fnn)).
   e. Let lane_3* be $ext(1, $size(Fnn), S, $feq($size(Fnn), lane_1, lane_2))*.
   f. Let v128 be $invlanes_((Inn X N), lane_3*).
   g. Return v128.
@@ -2267,7 +2267,7 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
   a. Let Fnn be lanet_u1.
   b. Let lane_1* be $lanes_((Fnn X N), v128_1).
   c. Let lane_2* be $lanes_((Fnn X N), v128_2).
-  d. Let Inn be $inverse_of_isize($size(Fnn)).
+  d. Let Inn be $isize^-1($size(Fnn)).
   e. Let lane_3* be $ext(1, $size(Fnn), S, $fne($size(Fnn), lane_1, lane_2))*.
   f. Let v128 be $invlanes_((Inn X N), lane_3*).
   g. Return v128.
@@ -2275,7 +2275,7 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
   a. Let Fnn be lanet_u1.
   b. Let lane_1* be $lanes_((Fnn X N), v128_1).
   c. Let lane_2* be $lanes_((Fnn X N), v128_2).
-  d. Let Inn be $inverse_of_isize($size(Fnn)).
+  d. Let Inn be $isize^-1($size(Fnn)).
   e. Let lane_3* be $ext(1, $size(Fnn), S, $flt($size(Fnn), lane_1, lane_2))*.
   f. Let v128 be $invlanes_((Inn X N), lane_3*).
   g. Return v128.
@@ -2283,7 +2283,7 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
   a. Let Fnn be lanet_u1.
   b. Let lane_1* be $lanes_((Fnn X N), v128_1).
   c. Let lane_2* be $lanes_((Fnn X N), v128_2).
-  d. Let Inn be $inverse_of_isize($size(Fnn)).
+  d. Let Inn be $isize^-1($size(Fnn)).
   e. Let lane_3* be $ext(1, $size(Fnn), S, $fgt($size(Fnn), lane_1, lane_2))*.
   f. Let v128 be $invlanes_((Inn X N), lane_3*).
   g. Return v128.
@@ -2291,7 +2291,7 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
   a. Let Fnn be lanet_u1.
   b. Let lane_1* be $lanes_((Fnn X N), v128_1).
   c. Let lane_2* be $lanes_((Fnn X N), v128_2).
-  d. Let Inn be $inverse_of_isize($size(Fnn)).
+  d. Let Inn be $isize^-1($size(Fnn)).
   e. Let lane_3* be $ext(1, $size(Fnn), S, $fle($size(Fnn), lane_1, lane_2))*.
   f. Let v128 be $invlanes_((Inn X N), lane_3*).
   g. Return v128.
@@ -2300,7 +2300,7 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
 11. Let Fnn be lanet_u1.
 12. Let lane_1* be $lanes_((Fnn X N), v128_1).
 13. Let lane_2* be $lanes_((Fnn X N), v128_2).
-14. Let Inn be $inverse_of_isize($size(Fnn)).
+14. Let Inn be $isize^-1($size(Fnn)).
 15. Let lane_3* be $ext(1, $size(Fnn), S, $fge($size(Fnn), lane_1, lane_2))*.
 16. Let v128 be $invlanes_((Inn X N), lane_3*).
 17. Return v128.
@@ -2363,7 +2363,7 @@ vcvtop (lanet_u0 X N_1) (lanet_u1 X N_2) vcvto_u4 sx_u5? lane__u3
 
 vextunop (Inn_1 X N_1) (Inn_2 X N_2) EXTADD_PAIRWISE sx c_1
 1. Let ci* be $lanes_((Inn_2 X N_2), c_1).
-2. Let [cj_1, cj_2]* be $inverse_of_concat_($ext($lsize(Inn_2), $lsize(Inn_1), sx, ci)*).
+2. Let [cj_1, cj_2]* be $concat_^-1($ext($lsize(Inn_2), $lsize(Inn_1), sx, ci)*).
 3. Let c be $invlanes_((Inn_1 X N_1), $iadd($lsize(Inn_1), cj_1, cj_2)*).
 4. Return c.
 
@@ -2377,7 +2377,7 @@ vextbinop (Inn_1 X N_1) (Inn_2 X N_2) vextb_u0 sx c_1 c_2
 2. Assert: Due to validation, (vextb_u0 is DOT).
 3. Let ci_1* be $lanes_((Inn_2 X N_2), c_1).
 4. Let ci_2* be $lanes_((Inn_2 X N_2), c_2).
-5. Let [cj_1, cj_2]* be $inverse_of_concat_($imul($lsize(Inn_1), $ext($lsize(Inn_2), $lsize(Inn_1), S, ci_1), $ext($lsize(Inn_2), $lsize(Inn_1), S, ci_2))*).
+5. Let [cj_1, cj_2]* be $concat_^-1($imul($lsize(Inn_1), $ext($lsize(Inn_2), $lsize(Inn_1), S, ci_1), $ext($lsize(Inn_2), $lsize(Inn_1), S, ci_2))*).
 6. Let c be $invlanes_((Inn_1 X N_1), $iadd($lsize(Inn_1), cj_1, cj_2)*).
 7. Return c.
 
@@ -3036,7 +3036,7 @@ execution_of_VBITMASK (Jnn X N)
 1. Assert: Due to validation, a value is on the top of the stack.
 2. Pop the value (V128.CONST c) from the stack.
 3. Let ci_1* be $lanes_((Jnn X N), c).
-4. Let ci be $inverse_of_ibits(32, $ilt($lsize(Jnn), S, ci_1, 0)*).
+4. Let ci be $ibits_1^-1(32, $ilt($lsize(Jnn), S, ci_1, 0)*).
 5. Push the value (I32.CONST ci) to the stack.
 
 execution_of_VSWIZZLE (Pnn X N)
@@ -3315,7 +3315,7 @@ execution_of_LOAD numty_u0 sz_sx_u1? ao
   a. Let nt be numty_u0.
   b. If (((i + ao.OFFSET) + ($size(nt) / 8)) > |$mem(z, 0).BYTES|), then:
     1) Trap.
-  c. Let c be $inverse_of_nbytes(nt, $mem(z, 0).BYTES[(i + ao.OFFSET) : ($size(nt) / 8)]).
+  c. Let c be $nbytes_1^-1(nt, $mem(z, 0).BYTES[(i + ao.OFFSET) : ($size(nt) / 8)]).
   d. Push the value (nt.CONST c) to the stack.
 5. If the type of numty_u0 is Inn, then:
   a. If sz_sx_u1? is defined, then:
@@ -3327,7 +3327,7 @@ execution_of_LOAD numty_u0 sz_sx_u1? ao
   c. If sz_sx_u1? is defined, then:
     1) Let ?(y_0) be sz_sx_u1?.
     2) Let (n, sx) be y_0.
-    3) Let c be $inverse_of_ibytes(n, $mem(z, 0).BYTES[(i + ao.OFFSET) : (n / 8)]).
+    3) Let c be $ibytes_1^-1(n, $mem(z, 0).BYTES[(i + ao.OFFSET) : (n / 8)]).
     4) Push the value (Inn.CONST $ext(n, $size(Inn), sx, c)) to the stack.
 
 execution_of_VLOAD V128 vload_u0? ao
@@ -3337,7 +3337,7 @@ execution_of_VLOAD V128 vload_u0? ao
 4. If ((((i + ao.OFFSET) + ($size(V128) / 8)) > |$mem(z, 0).BYTES|) and vload_u0? is not defined), then:
   a. Trap.
 5. If vload_u0? is not defined, then:
-  a. Let c be $inverse_of_vbytes(V128, $mem(z, 0).BYTES[(i + ao.OFFSET) : ($size(V128) / 8)]).
+  a. Let c be $vbytes_1^-1(V128, $mem(z, 0).BYTES[(i + ao.OFFSET) : ($size(V128) / 8)]).
   b. Push the value (V128.CONST c) to the stack.
 6. Else:
   a. Let ?(y_0) be vload_u0?.
@@ -3345,9 +3345,9 @@ execution_of_VLOAD V128 vload_u0? ao
     1) Let (SHAPE M N sx) be y_0.
     2) If (((i + ao.OFFSET) + ((M · N) / 8)) > |$mem(z, 0).BYTES|), then:
       a) Trap.
-    3) If the type of $inverse_of_lsize((M · 2)) is Jnn, then:
-      a) Let Jnn be $inverse_of_lsize((M · 2)).
-      b) Let j^N be $inverse_of_ibytes(M, $mem(z, 0).BYTES[((i + ao.OFFSET) + ((k · M) / 8)) : (M / 8)])^(k<N).
+    3) If the type of $lsize^-1((M · 2)) is Jnn, then:
+      a) Let Jnn be $lsize^-1((M · 2)).
+      b) Let j^N be $ibytes_1^-1(M, $mem(z, 0).BYTES[((i + ao.OFFSET) + ((k · M) / 8)) : (M / 8)])^(k<N).
       c) Let c be $invlanes_((Jnn X N), $ext(M, $lsize(Jnn), sx, j)^N).
       d) Push the value (V128.CONST c) to the stack.
   c. If y_0 is of the case SPLAT, then:
@@ -3355,16 +3355,16 @@ execution_of_VLOAD V128 vload_u0? ao
     2) If (((i + ao.OFFSET) + (N / 8)) > |$mem(z, 0).BYTES|), then:
       a) Trap.
     3) Let M be (128 / N).
-    4) If the type of $inverse_of_lsize(N) is Jnn, then:
-      a) Let Jnn be $inverse_of_lsize(N).
-      b) Let j be $inverse_of_ibytes(N, $mem(z, 0).BYTES[(i + ao.OFFSET) : (N / 8)]).
+    4) If the type of $lsize^-1(N) is Jnn, then:
+      a) Let Jnn be $lsize^-1(N).
+      b) Let j be $ibytes_1^-1(N, $mem(z, 0).BYTES[(i + ao.OFFSET) : (N / 8)]).
       c) Let c be $invlanes_((Jnn X M), j^M).
       d) Push the value (V128.CONST c) to the stack.
   d. If y_0 is of the case ZERO, then:
     1) Let (ZERO N) be y_0.
     2) If (((i + ao.OFFSET) + (N / 8)) > |$mem(z, 0).BYTES|), then:
       a) Trap.
-    3) Let j be $inverse_of_ibytes(N, $mem(z, 0).BYTES[(i + ao.OFFSET) : (N / 8)]).
+    3) Let j be $ibytes_1^-1(N, $mem(z, 0).BYTES[(i + ao.OFFSET) : (N / 8)]).
     4) Let c be $ext(N, 128, U, j).
     5) Push the value (V128.CONST c) to the stack.
 
@@ -3377,9 +3377,9 @@ execution_of_VLOAD_LANE V128 N ao j
 6. If (((i + ao.OFFSET) + (N / 8)) > |$mem(z, 0).BYTES|), then:
   a. Trap.
 7. Let M be (128 / N).
-8. If the type of $inverse_of_lsize(N) is Jnn, then:
-  a. Let Jnn be $inverse_of_lsize(N).
-  b. Let k be $inverse_of_ibytes(N, $mem(z, 0).BYTES[(i + ao.OFFSET) : (N / 8)]).
+8. If the type of $lsize^-1(N) is Jnn, then:
+  a. Let Jnn be $lsize^-1(N).
+  b. Let k be $ibytes_1^-1(N, $mem(z, 0).BYTES[(i + ao.OFFSET) : (N / 8)]).
   c. Let c be $invlanes_((Jnn X M), $lanes_((Jnn X M), c_1) with [j] replaced by k).
   d. Push the value (V128.CONST c) to the stack.
 
@@ -3549,8 +3549,8 @@ execution_of_VSTORE_LANE V128 N ao j
 6. If (((i + ao.OFFSET) + N) > |$mem(z, 0).BYTES|), then:
   a. Trap.
 7. Let M be (128 / N).
-8. If the type of $inverse_of_lsize(N) is Jnn, then:
-  a. Let Jnn be $inverse_of_lsize(N).
+8. If the type of $lsize^-1(N) is Jnn, then:
+  a. Let Jnn be $lsize^-1(N).
   b. If (j < |$lanes_((Jnn X M), c)|), then:
     1) Let b* be $ibytes(N, $lanes_((Jnn X M), c)[j]).
     2) Perform $with_mem(z, 0, (i + ao.OFFSET), (N / 8), b*).
@@ -5209,7 +5209,7 @@ signed N i
 4. Return (i - (2 ^ N)).
 
 invsigned N i
-1. Let j be $inverse_of_signed(N, i).
+1. Let j be $signed_1^-1(N, i).
 2. Return j.
 
 unop numty_u1 unop__u0 num__u3
@@ -5482,15 +5482,15 @@ cvtop numty_u1 numty_u4 cvtop_u0 num__u3
 11. Assert: Due to validation, the type of numty_u4 is Inn.
 12. Let Inn_2 be numty_u4.
 13. Let fN_1 be num__u3.
-14. Assert: Due to validation, the type of $inverse_of_sizenn2($sizenn1(Inn_1)) is Fnn.
+14. Assert: Due to validation, the type of $sizenn2^-1($sizenn1(Inn_1)) is Fnn.
 15. Return [$reinterpret(Fnn_1, Inn_2, fN_1)].
 
 invibytes N b*
-1. Let n be $inverse_of_ibytes(N, b*).
+1. Let n be $ibytes_1^-1(N, b*).
 2. Return n.
 
 invfbytes N b*
-1. Let p be $inverse_of_fbytes(N, b*).
+1. Let p be $fbytes_1^-1(N, b*).
 2. Return p.
 
 lpacknum lanet_u0 c
@@ -5522,7 +5522,7 @@ cunpacknum stora_u0 c
 4. Return $ext($psize(packtype), $size($lunpack(packtype)), U, c).
 
 invlanes_ sh c*
-1. Let vc be $inverse_of_lanes_(sh, c*).
+1. Let vc be $lanes__1^-1(sh, c*).
 2. Return vc.
 
 half (lanet_u1 X M_1) (lanet_u2 X M_2) half__u0 i j
@@ -5759,7 +5759,7 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
   a. Let Fnn be lanet_u1.
   b. Let lane_1* be $lanes_((Fnn X N), v128_1).
   c. Let lane_2* be $lanes_((Fnn X N), v128_2).
-  d. Let Inn be $inverse_of_isize($size(Fnn)).
+  d. Let Inn be $isize^-1($size(Fnn)).
   e. Let lane_3* be $ext(1, $size(Fnn), S, $feq($size(Fnn), lane_1, lane_2))*.
   f. Let v128 be $invlanes_((Inn X N), lane_3*).
   g. Return v128.
@@ -5767,7 +5767,7 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
   a. Let Fnn be lanet_u1.
   b. Let lane_1* be $lanes_((Fnn X N), v128_1).
   c. Let lane_2* be $lanes_((Fnn X N), v128_2).
-  d. Let Inn be $inverse_of_isize($size(Fnn)).
+  d. Let Inn be $isize^-1($size(Fnn)).
   e. Let lane_3* be $ext(1, $size(Fnn), S, $fne($size(Fnn), lane_1, lane_2))*.
   f. Let v128 be $invlanes_((Inn X N), lane_3*).
   g. Return v128.
@@ -5775,7 +5775,7 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
   a. Let Fnn be lanet_u1.
   b. Let lane_1* be $lanes_((Fnn X N), v128_1).
   c. Let lane_2* be $lanes_((Fnn X N), v128_2).
-  d. Let Inn be $inverse_of_isize($size(Fnn)).
+  d. Let Inn be $isize^-1($size(Fnn)).
   e. Let lane_3* be $ext(1, $size(Fnn), S, $flt($size(Fnn), lane_1, lane_2))*.
   f. Let v128 be $invlanes_((Inn X N), lane_3*).
   g. Return v128.
@@ -5783,7 +5783,7 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
   a. Let Fnn be lanet_u1.
   b. Let lane_1* be $lanes_((Fnn X N), v128_1).
   c. Let lane_2* be $lanes_((Fnn X N), v128_2).
-  d. Let Inn be $inverse_of_isize($size(Fnn)).
+  d. Let Inn be $isize^-1($size(Fnn)).
   e. Let lane_3* be $ext(1, $size(Fnn), S, $fgt($size(Fnn), lane_1, lane_2))*.
   f. Let v128 be $invlanes_((Inn X N), lane_3*).
   g. Return v128.
@@ -5791,7 +5791,7 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
   a. Let Fnn be lanet_u1.
   b. Let lane_1* be $lanes_((Fnn X N), v128_1).
   c. Let lane_2* be $lanes_((Fnn X N), v128_2).
-  d. Let Inn be $inverse_of_isize($size(Fnn)).
+  d. Let Inn be $isize^-1($size(Fnn)).
   e. Let lane_3* be $ext(1, $size(Fnn), S, $fle($size(Fnn), lane_1, lane_2))*.
   f. Let v128 be $invlanes_((Inn X N), lane_3*).
   g. Return v128.
@@ -5800,7 +5800,7 @@ vrelop (lanet_u1 X N) vrelo_u0 v128_1 v128_2
 11. Let Fnn be lanet_u1.
 12. Let lane_1* be $lanes_((Fnn X N), v128_1).
 13. Let lane_2* be $lanes_((Fnn X N), v128_2).
-14. Let Inn be $inverse_of_isize($size(Fnn)).
+14. Let Inn be $isize^-1($size(Fnn)).
 15. Let lane_3* be $ext(1, $size(Fnn), S, $fge($size(Fnn), lane_1, lane_2))*.
 16. Let v128 be $invlanes_((Inn X N), lane_3*).
 17. Return v128.
@@ -5863,7 +5863,7 @@ vcvtop (lanet_u0 X N_1) (lanet_u1 X N_2) vcvto_u6 sx_u7? lane__u3
 
 vextunop (Jnn_1 X N_1) (Jnn_2 X N_2) EXTADD_PAIRWISE sx c_1
 1. Let ci* be $lanes_((Jnn_1 X N_1), c_1).
-2. Let [cj_1, cj_2]* be $inverse_of_concat_($ext($lsize(Jnn_1), $lsize(Jnn_2), sx, ci)*).
+2. Let [cj_1, cj_2]* be $concat_^-1($ext($lsize(Jnn_1), $lsize(Jnn_2), sx, ci)*).
 3. Let c be $invlanes_((Jnn_2 X N_2), $iadd($lsize(Jnn_2), cj_1, cj_2)*).
 4. Return c.
 
@@ -5877,7 +5877,7 @@ vextbinop (Jnn_1 X N_1) (Jnn_2 X N_2) vextb_u0 sx c_1 c_2
 2. Assert: Due to validation, (vextb_u0 is DOT).
 3. Let ci_1* be $lanes_((Jnn_1 X N_1), c_1).
 4. Let ci_2* be $lanes_((Jnn_1 X N_1), c_2).
-5. Let [cj_1, cj_2]* be $inverse_of_concat_($imul($lsize(Jnn_2), $ext($lsize(Jnn_1), $lsize(Jnn_2), S, ci_1), $ext($lsize(Jnn_1), $lsize(Jnn_2), S, ci_2))*).
+5. Let [cj_1, cj_2]* be $concat_^-1($imul($lsize(Jnn_2), $ext($lsize(Jnn_1), $lsize(Jnn_2), S, ci_1), $ext($lsize(Jnn_1), $lsize(Jnn_2), S, ci_2))*).
 6. Let c be $invlanes_((Jnn_2 X N_2), $iadd($lsize(Jnn_2), cj_1, cj_2)*).
 7. Return c.
 
@@ -6720,7 +6720,7 @@ execution_of_VBITMASK (Jnn X M)
 1. Assert: Due to validation, a value is on the top of the stack.
 2. Pop the value (V128.CONST c) from the stack.
 3. Let ci_1* be $lanes_((Jnn X M), c).
-4. Let ci be $inverse_of_ibits(32, $ilt($lsize(Jnn), S, ci_1, 0)*).
+4. Let ci be $ibits_1^-1(32, $ilt($lsize(Jnn), S, ci_1, 0)*).
 5. Push the value (I32.CONST ci) to the stack.
 
 execution_of_VSWIZZLE (Pnn X M)
@@ -7033,9 +7033,10 @@ execution_of_ARRAY.NEW_DATA x y
 8. Let (mut, zt) be y_0.
 9. If ((i + ((n · $zsize(zt)) / 8)) > |$data(z, y).BYTES|), then:
   a. Trap.
-10. Let $zbytes(zt, c)^n be $inverse_of_concat_($data(z, y).BYTES[i : ((n · $zsize(zt)) / 8)]).
-11. Push the values $const($cunpack(zt), $cunpacknum(zt, c))^n to the stack.
-12. Execute the instruction (ARRAY.NEW_FIXED x n).
+10. Let $zbytes(y_0, c)^n be $concat_^-1($data(z, y).BYTES[i : ((n · $zsize(zt)) / 8)]).
+11. If (y_0 is zt), then:
+  a. Push the values $const($cunpack(zt), $cunpacknum(zt, c))^n to the stack.
+  b. Execute the instruction (ARRAY.NEW_FIXED x n).
 
 execution_of_ARRAY.GET sx? x
 1. Let z be the current state.
@@ -7247,7 +7248,7 @@ execution_of_ARRAY.INIT_DATA x y
       a) Let (ARRAY y_0) be $expanddt($type(z, x)).
       b) Let (mut, zt) be y_0.
       c) Let (REF.ARRAY_ADDR a) be instr_u0.
-      d) Let c be $inverse_of_zbytes(zt, $data(z, y).BYTES[j : ($zsize(zt) / 8)]).
+      d) Let c be $zbytes_1^-1(zt, $data(z, y).BYTES[j : ($zsize(zt) / 8)]).
       e) Push the value (REF.ARRAY_ADDR a) to the stack.
       f) Push the value (I32.CONST i) to the stack.
       g) Push the value $const($cunpack(zt), $cunpacknum(zt, c)) to the stack.
@@ -7366,7 +7367,7 @@ execution_of_LOAD numty_u0 loado_u2? x ao
   a. Let nt be numty_u0.
   b. If (((i + ao.OFFSET) + ($size(nt) / 8)) > |$mem(z, x).BYTES|), then:
     1) Trap.
-  c. Let c be $inverse_of_nbytes(nt, $mem(z, x).BYTES[(i + ao.OFFSET) : ($size(nt) / 8)]).
+  c. Let c be $nbytes_1^-1(nt, $mem(z, x).BYTES[(i + ao.OFFSET) : ($size(nt) / 8)]).
   d. Push the value (nt.CONST c) to the stack.
 5. If the type of numty_u0 is Inn, then:
   a. If loado_u2? is defined, then:
@@ -7378,7 +7379,7 @@ execution_of_LOAD numty_u0 loado_u2? x ao
   c. If loado_u2? is defined, then:
     1) Let ?(y_0) be loado_u2?.
     2) Let (n, sx) be y_0.
-    3) Let c be $inverse_of_ibytes(n, $mem(z, x).BYTES[(i + ao.OFFSET) : (n / 8)]).
+    3) Let c be $ibytes_1^-1(n, $mem(z, x).BYTES[(i + ao.OFFSET) : (n / 8)]).
     4) Push the value (Inn.CONST $ext(n, $size(Inn), sx, c)) to the stack.
 
 execution_of_VLOAD V128 vload_u0? x ao
@@ -7388,7 +7389,7 @@ execution_of_VLOAD V128 vload_u0? x ao
 4. If ((((i + ao.OFFSET) + ($vsize(V128) / 8)) > |$mem(z, x).BYTES|) and vload_u0? is not defined), then:
   a. Trap.
 5. If vload_u0? is not defined, then:
-  a. Let c be $inverse_of_vbytes(V128, $mem(z, x).BYTES[(i + ao.OFFSET) : ($vsize(V128) / 8)]).
+  a. Let c be $vbytes_1^-1(V128, $mem(z, x).BYTES[(i + ao.OFFSET) : ($vsize(V128) / 8)]).
   b. Push the value (V128.CONST c) to the stack.
 6. Else:
   a. Let ?(y_0) be vload_u0?.
@@ -7396,9 +7397,9 @@ execution_of_VLOAD V128 vload_u0? x ao
     1) Let (SHAPE M K sx) be y_0.
     2) If (((i + ao.OFFSET) + ((M · K) / 8)) > |$mem(z, x).BYTES|), then:
       a) Trap.
-    3) If the type of $inverse_of_lsizenn((M · 2)) is Jnn, then:
-      a) Let Jnn be $inverse_of_lsizenn((M · 2)).
-      b) Let j^K be $inverse_of_ibytes(M, $mem(z, x).BYTES[((i + ao.OFFSET) + ((k · M) / 8)) : (M / 8)])^(k<K).
+    3) If the type of $lsizenn^-1((M · 2)) is Jnn, then:
+      a) Let Jnn be $lsizenn^-1((M · 2)).
+      b) Let j^K be $ibytes_1^-1(M, $mem(z, x).BYTES[((i + ao.OFFSET) + ((k · M) / 8)) : (M / 8)])^(k<K).
       c) Let c be $invlanes_((Jnn X K), $ext(M, $lsizenn(Jnn), sx, j)^K).
       d) Push the value (V128.CONST c) to the stack.
   c. If y_0 is of the case SPLAT, then:
@@ -7406,16 +7407,16 @@ execution_of_VLOAD V128 vload_u0? x ao
     2) If (((i + ao.OFFSET) + (N / 8)) > |$mem(z, x).BYTES|), then:
       a) Trap.
     3) Let M be (128 / N).
-    4) If the type of $inverse_of_lsize(N) is Jnn, then:
-      a) Let Jnn be $inverse_of_lsize(N).
-      b) Let j be $inverse_of_ibytes(N, $mem(z, x).BYTES[(i + ao.OFFSET) : (N / 8)]).
+    4) If the type of $lsize^-1(N) is Jnn, then:
+      a) Let Jnn be $lsize^-1(N).
+      b) Let j be $ibytes_1^-1(N, $mem(z, x).BYTES[(i + ao.OFFSET) : (N / 8)]).
       c) Let c be $invlanes_((Jnn X M), j^M).
       d) Push the value (V128.CONST c) to the stack.
   d. If y_0 is of the case ZERO, then:
     1) Let (ZERO N) be y_0.
     2) If (((i + ao.OFFSET) + (N / 8)) > |$mem(z, x).BYTES|), then:
       a) Trap.
-    3) Let j be $inverse_of_ibytes(N, $mem(z, x).BYTES[(i + ao.OFFSET) : (N / 8)]).
+    3) Let j be $ibytes_1^-1(N, $mem(z, x).BYTES[(i + ao.OFFSET) : (N / 8)]).
     4) Let c be $ext(N, 128, U, j).
     5) Push the value (V128.CONST c) to the stack.
 
@@ -7428,9 +7429,9 @@ execution_of_VLOAD_LANE V128 N x ao j
 6. If (((i + ao.OFFSET) + (N / 8)) > |$mem(z, x).BYTES|), then:
   a. Trap.
 7. Let M be ($vsize(V128) / N).
-8. If the type of $inverse_of_lsize(N) is Jnn, then:
-  a. Let Jnn be $inverse_of_lsize(N).
-  b. Let k be $inverse_of_ibytes(N, $mem(z, x).BYTES[(i + ao.OFFSET) : (N / 8)]).
+8. If the type of $lsize^-1(N) is Jnn, then:
+  a. Let Jnn be $lsize^-1(N).
+  b. Let k be $ibytes_1^-1(N, $mem(z, x).BYTES[(i + ao.OFFSET) : (N / 8)]).
   c. Let c be $invlanes_((Jnn X M), $lanes_((Jnn X M), c_1) with [j] replaced by k).
   d. Push the value (V128.CONST c) to the stack.
 
@@ -7661,8 +7662,8 @@ execution_of_VSTORE_LANE V128 N x ao j
 6. If (((i + ao.OFFSET) + N) > |$mem(z, x).BYTES|), then:
   a. Trap.
 7. Let M be (128 / N).
-8. If the type of $inverse_of_lsize(N) is Jnn, then:
-  a. Let Jnn be $inverse_of_lsize(N).
+8. If the type of $lsize^-1(N) is Jnn, then:
+  a. Let Jnn be $lsize^-1(N).
   b. If (j < |$lanes_((Jnn X M), c)|), then:
     1) Let b* be $ibytes(N, $lanes_((Jnn X M), c)[j]).
     2) Perform $with_mem(z, x, (i + ao.OFFSET), (N / 8), b*).