diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -29,7 +29,7 @@
 
 ```bash
 cabal update
-cabal install --overwrite-policy=always phino-0.0.0.60
+cabal install --overwrite-policy=always phino-0.0.0.61
 phino --version
 ```
 
@@ -156,52 +156,24 @@
 
 ```bash
 $ cat bytes.phi
-{⟦
-  org ↦ ⟦
-    eolang ↦ ⟦
-      bytes ↦ ⟦
-        data ↦ ∅,
-        φ ↦ data
-      ⟧
-    ⟧
-  ⟧
-⟧}
+{⟦ bytes(data) ↦ ⟦ φ ↦ data ⟧ ⟧}
 $ cat number.phi
 {⟦
-  org ↦ ⟦
-    eolang ↦ ⟦
-      number ↦ ⟦
-        as-bytes ↦ ∅,
-        φ ↦ as-bytes,
-        plus(x) ↦ ⟦
-          λ ⤍ L_org_eolang_number_plus
-        ⟧
-      ⟧
-    ⟧
+  number(as-bytes) ↦ ⟦
+    φ ↦ as-bytes,
+    plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧
   ⟧
 ⟧}
-$ cat foo.phi
-{⟦
-  foo ↦ 5.plus(3)
-⟧}
-$ phino merge bytes.phi number.phi foo.phi --sweet
+$ cat minus.phi
+{⟦ number ↦ ⟦ minus(x) ↦ ⟦ λ ⤍ L_number_minus ⟧ ⟧ ⟧}
+$ phino merge bytes.phi number.phi minus.phi --sweet
 {⟦
-  org ↦ ⟦
-    eolang ↦ ⟦
-      bytes ↦ ⟦
-        data ↦ ∅,
-        φ ↦ data
-      ⟧,
-      number ↦ ⟦
-        as-bytes ↦ ∅,
-        φ ↦ as-bytes,
-        plus(x) ↦ ⟦
-          λ ⤍ L_org_eolang_number_plus
-        ⟧
-      ⟧
-    ⟧
-  ⟧,
-  foo ↦ 5.plus(3)
+  bytes(data) ↦ ⟦ φ ↦ data ⟧,
+  number(as-bytes) ↦ ⟦
+    φ ↦ as-bytes,
+    plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧,
+    minus(x) ↦ ⟦ λ ⤍ L_number_minus ⟧
+  ⟧
 ⟧}
 ```
 
@@ -216,18 +188,35 @@
 d >> 68-65-6C-6C-6F
 ```
 
-## Explain (under development)
+## Explain
 
 You can _explain_ rewriting rule by printing them in [LaTeX][latex] format:
 
 ```bash
-$ phino explain --rule=my-rule.yaml
-\documentclass{article}
-\usepackage{amsmath}
-\begin{document}
-\rule{My custom rule}
-\...
-\end{document}
+$ phino explain --normalize
+\begin{tabular}{rl}
+\trrule{ALPHA}
+  { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_2 -> e ) }
+  { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_1 -> e ) }
+  { if $ \indexof{ \tau_2 } = |B_1| $ }
+  { }
+\trrule{COPY}
+  { [[ B_1, \tau -> ?, B_2 ]] ( \tau -> e_1 ) }
+  { [[ B_1, \tau -> e_3, B_2 ]] }
+  { if $ \isnormal{ e_1 } $ }
+  { where $ e_2 \coloneqq \scopeof{ e_1 } $ and $ e_3 \coloneqq \ctx{ e_1 }{ e_2 } $ }
+\trrule{DC}
+  { T ( \tau -> e ) }
+  { T }
+  { }
+  { }
+...
+\trrule{STOP}
+  { [[ B ]] . \tau }
+  { T }
+  { if $ \tau \notin B \;\text{and}\; @ \notin B \;\text{and}\; L \notin B $ }
+  { }
+\end{tabular}
 ```
 
 For more details, use `phino [COMMAND] --help` option.
@@ -278,7 +267,7 @@
 
 Number:                  # comparable number
   = Integer              # just regular integer
-  | ordinal: Attribute'  # calculate index of alpha attribute
+  | index: Attribute'    # calculate index of alpha attribute
   | length: BiMeta'      # calculate length of bindings by given meta binding
 
 Extension:               # substitutions extension used to introduce new meta variables
@@ -322,13 +311,13 @@
   decimals accordingly. Uniqueness is guaranteed during one
   execution of `phino`.
 * `size` - accepts exactly one meta binding and returns size of it and
-  `Φ̇.number`.
-* `tau` - accepts `Φ̇.string`, dataizes it and converts it to attribute.
+  `Φ.number`.
+* `tau` - accepts `Φ.string`, dataizes it and converts it to attribute.
   If dataized string can't be converted to attribute - an error is thrown.
-* `string` - accepts `Φ̇.string` or `Φ̇.number` or attribute and converts it
-  to `Φ̇.string`.
-* `number` - accepts `Φ̇.string` and converts it `Φ̇.number`
-* `sum` - accepts list of `Φ̇.number` or `Φ̇.bytes` and returns sum of them as `Φ̇.number`
+* `string` - accepts `Φ.string` or `Φ.number` or attribute and converts it
+  to `Φ.string`.
+* `number` - accepts `Φ.string` and converts it `Φ.number`
+* `sum` - accepts list of `Φ.number` or `Φ.bytes` and returns sum of them as `Φ.number`
 * `join` - accepts list of bindings and returns list of joined bindings. Duplicated
   `ρ`, `Δ` and `λ` attributes are ignored, all other duplicated attributes are replaced
   with unique attributes using `random-tau` function.
diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: phino
-version: 0.0.0.61
+version: 0.0.0.62
 license: MIT
 synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions
 description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
diff --git a/resources/alpha.yaml b/resources/alpha.yaml
--- a/resources/alpha.yaml
+++ b/resources/alpha.yaml
@@ -6,5 +6,5 @@
 result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒)
 when:
   eq:
-    - ordinal: 𝜏2
+    - index: 𝜏2
     - length: 𝐵1
diff --git a/src/CST.hs b/src/CST.hs
--- a/src/CST.hs
+++ b/src/CST.hs
@@ -59,7 +59,7 @@
 data TERMINATION = DEAD | T
   deriving (Eq, Show)
 
-data SPACE = SPACE
+data SPACE = SPACE | NO_SPACE
   deriving (Eq, Show)
 
 data EOL = EOL | NO_EOL
@@ -105,7 +105,7 @@
   deriving (Eq, Show)
 
 data PROGRAM
-  = PR_SWEET {lcb :: LCB, expr :: EXPRESSION, rcb :: RCB}
+  = PR_SWEET {lcb :: LCB, expr :: EXPRESSION, rcb :: RCB, space :: SPACE}
   | PR_SALTY {global :: GLOBAL, arrow :: ARROW, expr :: EXPRESSION}
   deriving (Eq, Show)
 
@@ -154,10 +154,10 @@
   | EX_ATTR {attr :: ATTRIBUTE} -- sugar for $.x -> just x
   | EX_TERMINATION {termination :: TERMINATION}
   | EX_FORMATION {lsb :: LSB, eol :: EOL, tab :: TAB, binding :: BINDING, eol' :: EOL, tab' :: TAB, rsb :: RSB}
-  | EX_DISPATCH {expr :: EXPRESSION, attr :: ATTRIBUTE}
-  | EX_APPLICATION {expr :: EXPRESSION, eol :: EOL, tab :: TAB, tau :: APP_BINDING, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(a1 -> e1)
-  | EX_APPLICATION_TAUS {expr :: EXPRESSION, eol :: EOL, tab :: TAB, taus :: BINDING, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(a1 -> e1)(a2 -> e2)(...)
-  | EX_APPLICATION_EXPRS {expr :: EXPRESSION, eol :: EOL, tab :: TAB, args :: APP_ARG, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(e1, e2, ...)
+  | EX_DISPATCH {expr :: EXPRESSION, space :: SPACE, attr :: ATTRIBUTE}
+  | EX_APPLICATION {expr :: EXPRESSION, space :: SPACE, eol :: EOL, tab :: TAB, tau :: APP_BINDING, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(a1 -> e1)
+  | EX_APPLICATION_TAUS {expr :: EXPRESSION, space :: SPACE, eol :: EOL, tab :: TAB, taus :: BINDING, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(a1 -> e1)(a2 -> e2)(...)
+  | EX_APPLICATION_EXPRS {expr :: EXPRESSION, space :: SPACE, eol :: EOL, tab :: TAB, args :: APP_ARG, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(e1, e2, ...)
   | EX_STRING {str :: String, tab :: TAB, rhos :: [Binding]}
   | EX_NUMBER {num :: Either Int Double, tab :: TAB, rhos :: [Binding]}
   | EX_META {meta :: META}
@@ -198,7 +198,7 @@
   deriving (Eq, Show)
 
 data NUMBER
-  = ORDINAL {attr :: ATTRIBUTE}
+  = INDEX {attr :: ATTRIBUTE}
   | LENGTH {binding :: BINDING}
   | LITERAL {num :: Int}
   deriving (Eq, Show)
@@ -267,7 +267,7 @@
   toCST :: a -> (Int, EOL) -> b
 
 instance ToCST Program PROGRAM where
-  toCST (Program expr) ctx = PR_SWEET LCB (toCST expr ctx) RCB
+  toCST (Program expr) ctx = PR_SWEET LCB (toCST expr ctx) RCB NO_SPACE
 
 instance ToCST Expression EXPRESSION where
   toCST ExGlobal _ = EX_GLOBAL Φ
@@ -298,7 +298,7 @@
   toCST (DataString bts) (tabs, _) = EX_STRING (btsToStr bts) (TAB tabs) []
   toCST (DataNumber bts) (tabs, _) = EX_NUMBER (btsToNum bts) (TAB tabs) []
   toCST (ExDispatch ExThis attr) ctx = EX_ATTR (toCST attr ctx)
-  toCST (ExDispatch expr attr) ctx = EX_DISPATCH (toCST expr ctx) (toCST attr ctx)
+  toCST (ExDispatch expr attr) ctx = EX_DISPATCH (toCST expr ctx) NO_SPACE (toCST attr ctx)
   -- Since we convert AST to CST in sweet notation, here we're trying to get rid of unnecessary rho bindings
   -- in primitives (more details here: https://github.com/objectionary/phino/issues/451)
   -- If we find something similar to:
@@ -322,6 +322,7 @@
               then
                 EX_APPLICATION_TAUS
                   ex'
+                  NO_SPACE
                   eol
                   (TAB next)
                   (toCST ts (next, eol) :: BINDING)
@@ -331,6 +332,7 @@
               else
                 EX_APPLICATION_EXPRS
                   ex'
+                  NO_SPACE
                   eol
                   (TAB next)
                   (toCST exs (next, eol))
@@ -482,7 +484,7 @@
   toCST (Y.CmpNum num) _ = CMP_NUM (numberToCST num)
 
 instance ToCST Y.Number NUMBER where
-  toCST (Y.Ordinal attr) _ = ORDINAL (attributeToCST attr)
+  toCST (Y.Index attr) _ = INDEX (attributeToCST attr)
   toCST (Y.Length binding) _ = LENGTH (bindingsToCST [binding])
   toCST (Y.Literal num) _ = LITERAL num
 
diff --git a/src/Condition.hs b/src/Condition.hs
--- a/src/Condition.hs
+++ b/src/Condition.hs
@@ -49,10 +49,10 @@
 number =
   choice
     [ do
-        _ <- symbol "ordinal" >> lparen
+        _ <- symbol "index" >> lparen
         attr <- _attribute phiParser
         _ <- rparen
-        return (Y.Ordinal attr)
+        return (Y.Index attr)
     , do
         _ <- symbol "length" >> lparen
         bd <- _binding phiParser
diff --git a/src/Dataize.hs b/src/Dataize.hs
--- a/src/Dataize.hs
+++ b/src/Dataize.hs
@@ -154,7 +154,7 @@
         then morph (ExTermination, seq) ctx -- PRIM
         else do
           prog' <- withLocatedExpression _locator expr _program
-          (rewrittens', _) <- rewrite prog' normalizationRules (switchContext ctx) -- NMZ todo
+          (rewrittens', _) <- rewrite prog' normalizationRules (switchContext ctx) -- NMZ
           let seq' = reverse rewrittens' <> tail seq
           expr' <- locatedExpression _locator (fst (head seq'))
           morph (expr', seq') ctx
diff --git a/src/Encoding.hs b/src/Encoding.hs
--- a/src/Encoding.hs
+++ b/src/Encoding.hs
@@ -19,7 +19,7 @@
 
 instance ToASCII PROGRAM where
   toASCII PR_SALTY{..} = PR_SALTY Q ARROW' (toASCII expr)
-  toASCII PR_SWEET{..} = PR_SWEET lcb (toASCII expr) rcb
+  toASCII PR_SWEET{..} = PR_SWEET lcb (toASCII expr) rcb space
 
 instance ToASCII EXPRESSION where
   toASCII EX_GLOBAL{} = EX_GLOBAL Q
@@ -27,10 +27,10 @@
   toASCII EX_ATTR{..} = EX_ATTR (toASCII attr)
   toASCII EX_TERMINATION{} = EX_TERMINATION T
   toASCII EX_FORMATION{..} = EX_FORMATION LSB' eol tab (toASCII binding) eol' tab' RSB'
-  toASCII EX_DISPATCH{..} = EX_DISPATCH (toASCII expr) (toASCII attr)
-  toASCII EX_APPLICATION{..} = EX_APPLICATION (toASCII expr) eol tab (toASCII tau) eol' tab' indent
-  toASCII EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toASCII expr) eol tab (toASCII taus) eol' tab' indent
-  toASCII EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toASCII expr) eol tab (toASCII args) eol' tab' indent
+  toASCII EX_DISPATCH{..} = EX_DISPATCH (toASCII expr) space (toASCII attr)
+  toASCII EX_APPLICATION{..} = EX_APPLICATION (toASCII expr) space eol tab (toASCII tau) eol' tab' indent
+  toASCII EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toASCII expr) space eol tab (toASCII taus) eol' tab' indent
+  toASCII EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toASCII expr) space eol tab (toASCII args) eol' tab' indent
   toASCII EX_META{..} = EX_META (META EXCL E' (rest meta))
   toASCII EX_META_TAIL{..} = EX_META_TAIL (toASCII expr) meta
   toASCII EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toASCII expr)
@@ -79,7 +79,7 @@
   toASCII ST_ATTRIBUTES{..} = ST_ATTRIBUTES (map toASCII attrs)
 
 instance ToASCII NUMBER where
-  toASCII ORDINAL{..} = ORDINAL (toASCII attr)
+  toASCII INDEX{..} = INDEX (toASCII attr)
   toASCII LENGTH{..} = LENGTH (toASCII binding)
   toASCII literal@LITERAL{} = literal
 
diff --git a/src/LaTeX.hs b/src/LaTeX.hs
--- a/src/LaTeX.hs
+++ b/src/LaTeX.hs
@@ -22,7 +22,7 @@
 import AST
 import CST
 import Data.List (intercalate, nub)
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromMaybe, isJust)
 import Encoding
 import Lining
 import Locator (locatedExpression)
@@ -34,6 +34,7 @@
 import Rewriter (Rewritten, Rewrittens)
 import Sugar (SugarType (SWEET), ToSalty, withSugarType)
 import Text.Printf (printf)
+import Text.Read (readMaybe)
 import qualified Yaml as Y
 
 data LatexContext = LatexContext
@@ -201,24 +202,24 @@
   toLaTeX :: a -> a
 
 instance ToLaTeX PROGRAM where
-  toLaTeX PR_SWEET{..} = PR_SWEET BIG_LCB (toLaTeX expr) BIG_RCB
+  toLaTeX PR_SWEET{..} = PR_SWEET BIG_LCB (toLaTeX expr) BIG_RCB SPACE
   toLaTeX PR_SALTY{..} = PR_SALTY global arrow (toLaTeX expr)
 
 instance ToLaTeX EXPRESSION where
   toLaTeX EX_ATTR{..} = EX_ATTR (toLaTeX attr)
   toLaTeX EX_FORMATION{..} = EX_FORMATION lsb eol tab (toLaTeX binding) eol' tab' rsb
-  toLaTeX EX_APPLICATION{..} = EX_APPLICATION (toLaTeX expr) eol tab (toLaTeX tau) eol' tab' indent
-  toLaTeX EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toLaTeX expr) eol tab (toLaTeX taus) eol' tab' indent
-  toLaTeX EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toLaTeX expr) eol tab (toLaTeX args) eol' tab' indent
-  toLaTeX EX_DISPATCH{..} = EX_DISPATCH (toLaTeX expr) (toLaTeX attr)
+  toLaTeX EX_APPLICATION{..} = EX_APPLICATION (toLaTeX expr) SPACE eol tab (toLaTeX tau) eol' tab' indent
+  toLaTeX EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toLaTeX expr) SPACE eol tab (toLaTeX taus) eol' tab' indent
+  toLaTeX EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toLaTeX expr) SPACE eol tab (toLaTeX args) eol' tab' indent
+  toLaTeX EX_DISPATCH{..} = EX_DISPATCH (toLaTeX expr) SPACE (toLaTeX attr)
   toLaTeX EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toLaTeX expr)
   toLaTeX EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toLaTeX expr)
-  toLaTeX EX_META{..} = EX_META (META NO_EXCL E' (rest meta))
+  toLaTeX EX_META{..} = EX_META (toLaTeX meta)
   toLaTeX expr = expr
 
 instance ToLaTeX ATTRIBUTE where
   toLaTeX AT_LABEL{..} = AT_LABEL (piped (toLaTeX label))
-  toLaTeX AT_META{..} = AT_META (META NO_EXCL TAU' (rest meta))
+  toLaTeX AT_META{..} = AT_META (toLaTeX meta)
   toLaTeX AT_LAMBDA{} = AT_LAMBDA LAMBDA'
   toLaTeX AT_REST{} = AT_REST DOTS'
   toLaTeX attr = attr
@@ -228,12 +229,12 @@
 
 instance ToLaTeX BINDING where
   toLaTeX BI_PAIR{..} = BI_PAIR (toLaTeX pair) (toLaTeX bindings) tab
-  toLaTeX BI_META{..} = BI_META (META NO_EXCL B' (rest meta)) (toLaTeX bindings) tab
+  toLaTeX BI_META{..} = BI_META (toLaTeX meta) (toLaTeX bindings) tab
   toLaTeX bd = bd
 
 instance ToLaTeX BINDINGS where
   toLaTeX BDS_PAIR{..} = BDS_PAIR eol tab (toLaTeX pair) (toLaTeX bindings)
-  toLaTeX BDS_META{..} = BDS_META eol tab (META NO_EXCL B' (rest meta)) (toLaTeX bindings)
+  toLaTeX BDS_META{..} = BDS_META eol tab (toLaTeX meta) (toLaTeX bindings)
   toLaTeX bds = bds
 
 instance ToLaTeX PAIR where
@@ -244,11 +245,25 @@
   toLaTeX PA_TAU{..} = PA_TAU (toLaTeX attr) arrow (toLaTeX expr)
   toLaTeX PA_FORMATION{..} = PA_FORMATION (toLaTeX attr) (map toLaTeX voids) arrow (toLaTeX expr)
   toLaTeX PA_META_DELTA{..} = toLaTeX (PA_META_DELTA' meta)
-  toLaTeX PA_META_DELTA'{..} = PA_META_DELTA' (META NO_EXCL D' (rest meta))
+  toLaTeX PA_META_DELTA'{..} = PA_META_DELTA' (toLaTeX meta)
   toLaTeX PA_META_LAMBDA{..} = toLaTeX (PA_META_LAMBDA' meta)
-  toLaTeX PA_META_LAMBDA'{..} = PA_META_LAMBDA' (META NO_EXCL F (rest meta))
+  toLaTeX PA_META_LAMBDA'{..} = PA_META_LAMBDA' (toLaTeX meta)
   toLaTeX pair = pair
 
+instance ToLaTeX META where
+  toLaTeX META{..} =
+    let idx = readMaybe rest :: Maybe Int
+        rest' = if not (null rest) && length rest <= 2 && isJust idx then '_' : rest else rest
+     in META NO_EXCL (toLaTeX hd) rest'
+
+instance ToLaTeX META_HEAD where
+  toLaTeX E = E'
+  toLaTeX A = TAU'
+  toLaTeX TAU = TAU'
+  toLaTeX B = B'
+  toLaTeX D = D'
+  toLaTeX mh = mh
+
 instance ToLaTeX APP_ARG where
   toLaTeX APP_ARG{..} = APP_ARG (toLaTeX expr) (toLaTeX args)
 
@@ -273,7 +288,7 @@
   toLaTeX ST_ATTRIBUTES{..} = ST_ATTRIBUTES (map toLaTeX attrs)
 
 instance ToLaTeX NUMBER where
-  toLaTeX ORDINAL{..} = ORDINAL (toLaTeX attr)
+  toLaTeX INDEX{..} = INDEX (toLaTeX attr)
   toLaTeX LENGTH{..} = LENGTH (toLaTeX binding)
   toLaTeX literal@LITERAL{} = literal
 
@@ -316,12 +331,12 @@
     conditionToLatex Nothing = "{ }"
     conditionToLatex (Just cond) = case conditionToCST cond of
       CO_EMPTY -> "{ }"
-      cond' -> braced ("if " <> renderToLatex cond' defaultLatexContext)
+      cond' -> braced ("if $ " <> renderToLatex cond' defaultLatexContext <> " $")
     extraArgumentsToLatex :: Maybe [Y.Extra] -> String
     extraArgumentsToLatex Nothing = "{ }"
     extraArgumentsToLatex (Just extras) =
       let extras' = map ((`renderToLatex` defaultLatexContext) . extraToCST) extras
-       in braced ("where " <> intercalate "; " extras')
+       in braced ("where " <> intercalate " and " extras')
     braced :: String -> String
     braced = printf "{ %s }"
     -- Join two maybe conditions into single one using Y.And if at least one is just.
diff --git a/src/Lining.hs b/src/Lining.hs
--- a/src/Lining.hs
+++ b/src/Lining.hs
@@ -20,15 +20,15 @@
 
 instance ToSingleLine PROGRAM where
   toSingleLine PR_SALTY{..} = PR_SALTY global arrow (toSingleLine expr)
-  toSingleLine PR_SWEET{..} = PR_SWEET lcb (toSingleLine expr) rcb
+  toSingleLine PR_SWEET{..} = PR_SWEET lcb (toSingleLine expr) rcb space
 
 instance ToSingleLine EXPRESSION where
   toSingleLine EX_FORMATION{lsb, binding = bd@BI_EMPTY{}, rsb} = EX_FORMATION lsb NO_EOL NO_TAB bd NO_EOL NO_TAB rsb
   toSingleLine EX_FORMATION{..} = EX_FORMATION lsb NO_EOL TAB' (toSingleLine binding) NO_EOL TAB' rsb
-  toSingleLine EX_DISPATCH{..} = EX_DISPATCH (toSingleLine expr) attr
-  toSingleLine EX_APPLICATION{..} = EX_APPLICATION (toSingleLine expr) NO_EOL TAB' (toSingleLine tau) NO_EOL TAB' indent
-  toSingleLine EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toSingleLine expr) NO_EOL TAB' (toSingleLine taus) NO_EOL TAB' indent
-  toSingleLine EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toSingleLine expr) NO_EOL TAB' (toSingleLine args) NO_EOL TAB' indent
+  toSingleLine EX_DISPATCH{..} = EX_DISPATCH (toSingleLine expr) space attr
+  toSingleLine EX_APPLICATION{..} = EX_APPLICATION (toSingleLine expr) space NO_EOL TAB' (toSingleLine tau) NO_EOL TAB' indent
+  toSingleLine EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toSingleLine expr) space NO_EOL TAB' (toSingleLine taus) NO_EOL TAB' indent
+  toSingleLine EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toSingleLine expr) space NO_EOL TAB' (toSingleLine args) NO_EOL TAB' indent
   toSingleLine EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSingleLine expr)
   toSingleLine EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toSingleLine expr)
   toSingleLine expr = expr
diff --git a/src/Margin.hs b/src/Margin.hs
--- a/src/Margin.hs
+++ b/src/Margin.hs
@@ -21,7 +21,7 @@
   withMargin' :: (Int, Int) -> a -> a
 
 instance WithMargin PROGRAM where
-  withMargin' (_, margin) PR_SWEET{..} = PR_SWEET lcb (withMargin' (2, margin) expr) rcb
+  withMargin' (_, margin) PR_SWEET{..} = PR_SWEET lcb (withMargin' (2, margin) expr) rcb space
   withMargin' (_, margin) PR_SALTY{..} =
     let before = lengthOf global + lengthOf arrow + 2 -- 'Q -> '
      in PR_SALTY global arrow (withMargin' (before, margin) expr)
@@ -34,7 +34,7 @@
      in if lengthOf single + extra <= margin then single else ex'
   withMargin' _ num@EX_NUMBER{} = num
   withMargin' _ str@EX_STRING{} = str
-  withMargin' cfg EX_DISPATCH{..} = EX_DISPATCH (withMargin' cfg expr) attr
+  withMargin' cfg EX_DISPATCH{..} = EX_DISPATCH (withMargin' cfg expr) space attr
   withMargin' cfg EX_META_TAIL{..} = EX_META_TAIL (withMargin' cfg expr) meta
   withMargin' cfg EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (withMargin' cfg expr)
   withMargin' cfg EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (withMargin' cfg expr)
@@ -47,9 +47,9 @@
         singleArg = toSingleLine arg
      in if
           | lengthOf single + extra <= margin -> single
-          | lengthOf singleMain + extra <= margin -> EX_APPLICATION singleMain EOL tab arg EOL tab' indent
-          | lengthOf singleArg + extra' <= margin -> EX_APPLICATION main NO_EOL TAB' singleArg NO_EOL TAB' indent
-          | otherwise -> EX_APPLICATION main EOL tab arg EOL tab' indent
+          | lengthOf singleMain + extra <= margin -> EX_APPLICATION singleMain space EOL tab arg EOL tab' indent
+          | lengthOf singleArg + extra' <= margin -> EX_APPLICATION main space NO_EOL TAB' singleArg NO_EOL TAB' indent
+          | otherwise -> EX_APPLICATION main space EOL tab arg EOL tab' indent
   withMargin' cfg@(extra, margin) ex@EX_APPLICATION_EXPRS{tab = tab@(TAB indt), ..} =
     let single = toSingleLine ex
         main = withMargin' cfg expr
@@ -59,9 +59,9 @@
         singleExprs = toSingleLine exprs
      in if
           | lengthOf single + extra <= margin -> single
-          | lengthOf singleMain + extra <= margin -> EX_APPLICATION_EXPRS singleMain EOL tab exprs EOL tab' indent
-          | lengthOf singleExprs + extra' <= margin -> EX_APPLICATION_EXPRS main NO_EOL TAB' singleExprs NO_EOL TAB' indent
-          | otherwise -> EX_APPLICATION_EXPRS main EOL tab exprs EOL tab' indent
+          | lengthOf singleMain + extra <= margin -> EX_APPLICATION_EXPRS singleMain space EOL tab exprs EOL tab' indent
+          | lengthOf singleExprs + extra' <= margin -> EX_APPLICATION_EXPRS main space NO_EOL TAB' singleExprs NO_EOL TAB' indent
+          | otherwise -> EX_APPLICATION_EXPRS main space EOL tab exprs EOL tab' indent
   withMargin' cfg@(extra, margin) ex@EX_APPLICATION_TAUS{tab = tab@(TAB indt), ..} =
     let single = toSingleLine ex
         main = withMargin' cfg expr
@@ -71,9 +71,9 @@
         singleTaus = toSingleLine taus'
      in if
           | lengthOf single + extra <= margin -> single
-          | lengthOf singleMain + extra <= margin -> EX_APPLICATION_TAUS singleMain EOL tab taus' EOL tab' indent
-          | lengthOf singleTaus + extra' <= margin -> EX_APPLICATION_TAUS main NO_EOL TAB' singleTaus NO_EOL TAB' indent
-          | otherwise -> EX_APPLICATION_TAUS main EOL tab taus' EOL tab' indent
+          | lengthOf singleMain + extra <= margin -> EX_APPLICATION_TAUS singleMain space EOL tab taus' EOL tab' indent
+          | lengthOf singleTaus + extra' <= margin -> EX_APPLICATION_TAUS main space NO_EOL TAB' singleTaus NO_EOL TAB' indent
+          | otherwise -> EX_APPLICATION_TAUS main space EOL tab taus' EOL tab' indent
   withMargin' _ ex = ex
 
 instance WithMargin APP_BINDING where
diff --git a/src/Render.hs b/src/Render.hs
--- a/src/Render.hs
+++ b/src/Render.hs
@@ -77,7 +77,7 @@
 
 instance Render LAMBDA where
   render LAMBDA = "λ"
-  render LAMBDA' = "\\lambda"
+  render LAMBDA' = "L"
 
 instance Render GLOBAL where
   render Φ = "Φ"
@@ -89,6 +89,7 @@
 
 instance Render SPACE where
   render SPACE = " "
+  render NO_SPACE = ""
 
 instance Render EOL where
   render EOL = "\n"
@@ -134,7 +135,7 @@
   render NO_TAB = ""
 
 instance Render PROGRAM where
-  render PR_SWEET{..} = render lcb <> render expr <> render rcb
+  render PR_SWEET{..} = render lcb <> render space <> render expr <> render space <> render rcb
   render PR_SALTY{..} = render global <> render SPACE <> render arrow <> render SPACE <> render expr
 
 instance Render PAIR where
@@ -177,10 +178,10 @@
   render EX_ATTR{..} = render attr
   render EX_TERMINATION{..} = render termination
   render EX_FORMATION{..} = render lsb <> render eol <> render tab <> render binding <> render eol' <> render tab' <> render rsb
-  render EX_DISPATCH{..} = render expr <> "." <> render attr
-  render EX_APPLICATION{..} = render expr <> "(" <> render eol <> render tab <> render tau <> render eol' <> render tab' <> ")"
-  render EX_APPLICATION_TAUS{..} = render expr <> "(" <> render eol <> render tab <> render taus <> render eol' <> render tab' <> ")"
-  render EX_APPLICATION_EXPRS{..} = render expr <> "(" <> render eol <> render tab <> render args <> render eol' <> render tab' <> ")"
+  render EX_DISPATCH{..} = render expr <> render space <> "." <> render space <> render attr
+  render EX_APPLICATION{..} = render expr <> render space <> "(" <> render eol <> render tab <> render tau <> render eol' <> render tab' <> ")"
+  render EX_APPLICATION_TAUS{..} = render expr <> render space <> "(" <> render eol <> render tab <> render taus <> render eol' <> render tab' <> ")"
+  render EX_APPLICATION_EXPRS{..} = render expr <> render space <> "(" <> render eol <> render tab <> render args <> render eol' <> render tab' <> ")"
   render EX_STRING{..} = '"' : render str <> "\""
   render EX_NUMBER{..} = either show show num
   render EX_META{..} = render meta
@@ -210,12 +211,12 @@
   render ST_ATTRIBUTES{..} = printf "[ %s ]" (intercalate ", " (map render attrs))
 
 instance Render LOGIC_OPERATOR where
-  render AND = "and"
-  render OR = "or"
+  render AND = "\\;\\text{and}\\;"
+  render OR = "\\;\\text{or}\\;"
 
 instance Render NUMBER where
-  render ORDINAL{..} = renderFunc "ordinal" attr
-  render LENGTH{..} = renderFunc "length" binding
+  render INDEX{..} = printf "\\indexof{ %s }" (render attr)
+  render LENGTH{..} = printf "|%s|" (render binding)
   render LITERAL{..} = show num
 
 instance Render COMPARABLE where
@@ -230,8 +231,13 @@
 instance Render CONDITION where
   render CO_BELONGS{..} = render attr <> render SPACE <> render belongs <> render SPACE <> render set
   render CO_LOGIC{conditions = [cond]} = render cond
-  render CO_LOGIC{..} = printf "\\( %s \\)" (intercalate (printf " \\) %s \\( " (render operator)) (map render conditions))
-  render CO_NF{..} = renderFunc "NF" expr
+  render CO_LOGIC{..} = intercalate (printf " %s " (render operator)) (map renderWrapped conditions)
+    where
+      renderWrapped :: CONDITION -> String
+      renderWrapped CO_LOGIC{conditions = [cond]} = render cond
+      renderWrapped cond@CO_LOGIC{} = printf "( %s )" (render cond)
+      renderWrapped cond = render cond
+  render CO_NF{..} = printf "\\isnormal{ %s }" (render expr)
   render CO_NOT{..} = renderFunc "not" condition
   render CO_COMPARE{..} = render left <> render SPACE <> render equal <> render SPACE <> render right
   render CO_MATCHES{..} = printf "matches( %s, %s )" regex (render expr)
@@ -248,4 +254,6 @@
   render ARG_BYTES{..} = render bytes
 
 instance Render EXTRA where
-  render EXTRA{..} = render meta <> " <- " <> printf "%s( %s )" func (intercalate ", " (map render args))
+  render EXTRA{func = "contextualize", ..} = printf "$ %s \\coloneqq \\ctx{ %s }{ %s } $" (render meta) (render (head args)) (intercalate ", " (map render (tail args)))
+  render EXTRA{func = "scope", ..} = printf "$ %s \\coloneqq \\scopeof{ %s } $" (render meta) (render (head args))
+  render EXTRA{..} = printf "$ %s \\coloneqq %s( %s ) $" (render meta) func (intercalate ", " (map render args))
diff --git a/src/Rule.hs b/src/Rule.hs
--- a/src/Rule.hs
+++ b/src/Rule.hs
@@ -122,10 +122,10 @@
   where
     -- Convert Number to Int
     numToInt :: Y.Number -> Subst -> Maybe Int
-    numToInt (Y.Ordinal (AtMeta meta)) (Subst mp) = case M.lookup meta mp of
+    numToInt (Y.Index (AtMeta meta)) (Subst mp) = case M.lookup meta mp of
       Just (MvAttribute (AtAlpha idx)) -> Just idx
       _ -> Nothing
-    numToInt (Y.Ordinal (AtAlpha idx)) _ = Just idx
+    numToInt (Y.Index (AtAlpha idx)) _ = Just idx
     numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of
       Just (MvBindings bds) -> Just (length bds)
       _ -> Nothing
diff --git a/src/Sugar.hs b/src/Sugar.hs
--- a/src/Sugar.hs
+++ b/src/Sugar.hs
@@ -59,11 +59,11 @@
   toSalty prog = prog
 
 instance ToSalty EXPRESSION where
-  toSalty EX_ATTR{..} = EX_DISPATCH (EX_XI XI) attr
-  toSalty EX_DISPATCH{..} = EX_DISPATCH (toSalty expr) attr
+  toSalty EX_ATTR{..} = EX_DISPATCH (EX_XI XI) NO_SPACE attr
+  toSalty EX_DISPATCH{..} = EX_DISPATCH (toSalty expr) space attr
   toSalty EX_FORMATION{lsb, binding = bd@BI_EMPTY{}, rsb} = EX_FORMATION lsb NO_EOL TAB' (toSalty (bdWithVoidRho bd)) NO_EOL TAB' rsb
   toSalty EX_FORMATION{..} = EX_FORMATION lsb eol tab (toSalty (bdWithVoidRho binding)) eol' tab' rsb
-  toSalty EX_APPLICATION{..} = EX_APPLICATION (toSalty expr) EOL (TAB indent) (toSalty tau) EOL (TAB (indent - 1)) indent
+  toSalty EX_APPLICATION{..} = EX_APPLICATION (toSalty expr) space EOL (TAB indent) (toSalty tau) EOL (TAB (indent - 1)) indent
   toSalty EX_APPLICATION_TAUS{..} =
     foldl
       toApplication
@@ -72,7 +72,7 @@
     where
       toApplication :: EXPRESSION -> PAIR -> EXPRESSION
       toApplication exp pair =
-        EX_APPLICATION (toSalty exp) EOL (TAB indent) (APP_BINDING (toSalty pair)) EOL (TAB (indent - 1)) indent
+        EX_APPLICATION (toSalty exp) space EOL (TAB indent) (APP_BINDING (toSalty pair)) EOL (TAB (indent - 1)) indent
       tauToPairs :: BINDING -> [PAIR]
       tauToPairs BI_PAIR{..} = pair : tausToPairs bindings
       tauToPairs BI_EMPTY{} = []
@@ -81,7 +81,7 @@
       tausToPairs BDS_EMPTY{} = []
       tausToPairs BDS_PAIR{..} = pair : tausToPairs bindings
       tausToPairs (BDS_META _ _ mt _) = error $ "BDS_META " ++ show mt ++ " unexpected in tausToPairs"
-  toSalty EX_APPLICATION_EXPRS{..} = toSalty (EX_APPLICATION_TAUS expr EOL (TAB indent) (argToBinding args tab) EOL (TAB (indent - 1)) indent)
+  toSalty EX_APPLICATION_EXPRS{..} = toSalty (EX_APPLICATION_TAUS expr space EOL (TAB indent) (argToBinding args tab) EOL (TAB (indent - 1)) indent)
     where
       argToBinding :: APP_ARG -> TAB -> BINDING
       argToBinding APP_ARG{..} =
@@ -115,6 +115,7 @@
    in toSalty
         ( EX_APPLICATION_TAUS
             base
+            NO_SPACE
             EOL
             next
             ( BI_PAIR
@@ -123,6 +124,7 @@
                     ARROW
                     ( EX_APPLICATION_EXPRS
                         bytes
+                        NO_SPACE
                         EOL
                         (TAB (indent + 2))
                         (APP_ARG data' AAS_EMPTY)
diff --git a/src/Yaml.hs b/src/Yaml.hs
--- a/src/Yaml.hs
+++ b/src/Yaml.hs
@@ -54,9 +54,9 @@
 instance FromJSON Number where
   parseJSON v = case v of
     Object o -> do
-      validateYamlObject o ["ordinal", "length"]
+      validateYamlObject o ["index", "length"]
       asum
-        [ Ordinal <$> o .: "ordinal"
+        [ Index <$> o .: "index"
         , Length <$> o .: "length"
         ]
     Number num -> pure (Literal (round num))
@@ -132,7 +132,7 @@
         }
 
 data Number
-  = Ordinal Attribute
+  = Index Attribute
   | Length Binding
   | Literal Int
   deriving (Eq, Generic, Show)
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -359,15 +359,15 @@
           ["rewrite", "--output=latex", "--sweet"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{[["
-              , "  |x\\char95{}o| -> Q.|z|( |y| -> 5 ),"
+              , "\\Big\\{ [["
+              , "  |x\\char95{}o| -> Q . |z| ( |y| -> 5 ),"
               , "  |q\\char36{}| -> T,"
               , "  |w| -> $,"
               , "  ^ -> Q,"
               , "  @ -> 1,"
               , "  |y| -> \"H$@^M\","
               , "  L> |Fu\\char95{}nc|"
-              , "]]\\Big\\}{.}"
+              , "]] \\Big\\}{.}"
               , "\\end{phiquation}"
               ]
           ]
@@ -378,7 +378,7 @@
           ["rewrite", "--output=latex", "--sweet", "--nonumber", "--flat"]
           [ unlines
               [ "\\begin{phiquation*}"
-              , "\\Big\\{[[ |x| -> 5 ]]\\Big\\}{.}"
+              , "\\Big\\{ [[ |x| -> 5 ]] \\Big\\}{.}"
               , "\\end{phiquation*}"
               ]
           ]
@@ -389,7 +389,7 @@
           ["rewrite", "--output=latex", "--sweet", "--flat", "--expression=foo"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\phiExpression{foo} \\Big\\{[[ |x| -> 5 ]]\\Big\\}{.}"
+              , "\\phiExpression{foo} \\Big\\{ [[ |x| -> 5 ]] \\Big\\}{.}"
               , "\\end{phiquation}"
               ]
           ]
@@ -400,7 +400,7 @@
           ["rewrite", "--output=latex", "--sweet", "--flat", "--label=foo"]
           [ unlines
               [ "\\begin{phiquation}\n\\label{foo}"
-              , "\\Big\\{[[ |x| -> 5 ]]\\Big\\}{.}"
+              , "\\Big\\{ [[ |x| -> 5 ]] \\Big\\}{.}"
               , "\\end{phiquation}"
               ]
           ]
@@ -457,9 +457,9 @@
           ]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{[[ |x| -> \"foo\" ]]\\Big\\} \\leadsto_{\\nameref{r:first}}"
-              , "  \\leadsto \\Big\\{Q.|x|( |y| -> \"foo\" )\\Big\\} \\leadsto_{\\nameref{r:second}}"
-              , "  \\leadsto \\Big\\{[[ |x| -> \"foo\" ]]\\Big\\}{.}"
+              , "\\Big\\{ [[ |x| -> \"foo\" ]] \\Big\\} \\leadsto_{\\nameref{r:first}}"
+              , "  \\leadsto \\Big\\{ Q . |x| ( |y| -> \"foo\" ) \\Big\\} \\leadsto_{\\nameref{r:second}}"
+              , "  \\leadsto \\Big\\{ [[ |x| -> \"foo\" ]] \\Big\\}{.}"
               , "\\end{phiquation}"
               ]
           ]
@@ -470,12 +470,12 @@
           ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress", "--meet-prefix=foo"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{[[ |x| -> ?, |y| -> |x| ]]( |x| -> \\phiMeet{foo:1}{ [[ D> 42- ]] } ).|y|\\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{\\phiMeet{foo:2}{ [[ |x| -> \\phiAgain{foo:1}, |y| -> |x| ]] }.|y|\\Big\\} \\leadsto_{\\nameref{r:dot}}"
-              , "  \\leadsto \\Big\\{\\phiAgain{foo:2}.|x|( ^ -> \\phiAgain{foo:2} )\\Big\\} \\leadsto_{\\nameref{r:dot}}"
-              , "  \\leadsto \\Big\\{\\phiAgain{foo:1}( ^ -> \\phiAgain{foo:2}, ^ -> \\phiAgain{foo:2} )\\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{foo:2} ]]( ^ -> \\phiAgain{foo:2} )\\Big\\} \\leadsto_{\\nameref{r:stay}}"
-              , "  \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{foo:2} ]]\\Big\\}{.}"
+              , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phiMeet{foo:1}{ [[ D> 42- ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto \\Big\\{ \\phiMeet{foo:2}{ [[ |x| -> \\phiAgain{foo:1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}"
+              , "  \\leadsto \\Big\\{ \\phiAgain{foo:2} . |x| ( ^ -> \\phiAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}"
+              , "  \\leadsto \\Big\\{ \\phiAgain{foo:1} ( ^ -> \\phiAgain{foo:2}, ^ -> \\phiAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto \\Big\\{ [[ D> 42-, ^ -> \\phiAgain{foo:2} ]] ( ^ -> \\phiAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"
+              , "  \\leadsto \\Big\\{ [[ D> 42-, ^ -> \\phiAgain{foo:2} ]] \\Big\\}{.}"
               , "\\end{phiquation}"
               ]
           ]
@@ -486,12 +486,12 @@
           ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{[[ |x| -> ?, |y| -> |x| ]]( |x| -> \\phiMeet{1}{ [[ D> 42- ]] } ).|y|\\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{\\phiMeet{2}{ [[ |x| -> \\phiAgain{1}, |y| -> |x| ]] }.|y|\\Big\\} \\leadsto_{\\nameref{r:dot}}"
-              , "  \\leadsto \\Big\\{\\phiAgain{2}.|x|( ^ -> \\phiAgain{2} )\\Big\\} \\leadsto_{\\nameref{r:dot}}"
-              , "  \\leadsto \\Big\\{\\phiAgain{1}( ^ -> \\phiAgain{2}, ^ -> \\phiAgain{2} )\\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{2} ]]( ^ -> \\phiAgain{2} )\\Big\\} \\leadsto_{\\nameref{r:stay}}"
-              , "  \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{2} ]]\\Big\\}{.}"
+              , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phiMeet{1}{ [[ D> 42- ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto \\Big\\{ \\phiMeet{2}{ [[ |x| -> \\phiAgain{1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}"
+              , "  \\leadsto \\Big\\{ \\phiAgain{2} . |x| ( ^ -> \\phiAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}"
+              , "  \\leadsto \\Big\\{ \\phiAgain{1} ( ^ -> \\phiAgain{2}, ^ -> \\phiAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto \\Big\\{ [[ D> 42-, ^ -> \\phiAgain{2} ]] ( ^ -> \\phiAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"
+              , "  \\leadsto \\Big\\{ [[ D> 42-, ^ -> \\phiAgain{2} ]] \\Big\\}{.}"
               , "\\end{phiquation}"
               ]
           ]
@@ -502,9 +502,9 @@
           ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> \\phiMeet{1}{ [[ |t| -> 42 ]] } ]]( |y| -> \\phiAgain{1} ) ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> \\phiAgain{1}, |k| -> \\phiAgain{1} ]] ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:stop}}"
-              , "  \\leadsto \\Big\\{[[ |ex| -> T ]]\\Big\\}{.}"
+              , "\\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> \\phiMeet{1}{ [[ |t| -> 42 ]] } ]] ( |y| -> \\phiAgain{1} ) ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto \\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> \\phiAgain{1}, |k| -> \\phiAgain{1} ]] ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:stop}}"
+              , "  \\leadsto \\Big\\{ [[ |ex| -> T ]] \\Big\\}{.}"
               , "\\end{phiquation}"
               ]
           ]
@@ -515,9 +515,9 @@
           ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet", "--meet-popularity=70"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]]( |y| -> [[ |t| -> 42 ]] ) ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:stop}}"
-              , "  \\leadsto \\Big\\{[[ |ex| -> T ]]\\Big\\}{.}"
+              , "\\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto \\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:stop}}"
+              , "  \\leadsto \\Big\\{ [[ |ex| -> T ]] \\Big\\}{.}"
               , "\\end{phiquation}"
               ]
           ]
@@ -528,9 +528,9 @@
           ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet", "--meet-length=32"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]]( |y| -> [[ |t| -> 42 ]] ) ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:stop}}"
-              , "  \\leadsto \\Big\\{[[ |ex| -> T ]]\\Big\\}{.}"
+              , "\\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto \\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:stop}}"
+              , "  \\leadsto \\Big\\{ [[ |ex| -> T ]] \\Big\\}{.}"
               , "\\end{phiquation}"
               ]
           ]
@@ -541,8 +541,8 @@
           ["rewrite", "--normalize", "--sequence", "--flat", "--output=latex", "--sweet", "--focus=Q.ex"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "[[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]]( |y| -> [[ |t| -> 42 ]] ) ]].|i| \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]].|i| \\leadsto_{\\nameref{r:stop}}"
+              , "[[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| \\leadsto_{\\nameref{r:stop}}"
               , "  \\leadsto T{.}"
               , "\\end{phiquation}"
               ]
@@ -565,8 +565,8 @@
           ["rewrite", "--normalize", "--flat", "--sequence", "--output=latex", "--sweet", "--max-depth=1", "--max-cycles=1"]
           [ unlines
               [ "\\begin{phiquation}"
-              , "\\Big\\{[[ |x| -> |y|, |y| -> |x| ]].|x|\\Big\\} \\leadsto_{\\nameref{r:dot}}"
-              , "  \\leadsto \\Big\\{[[ |x| -> |y|, |y| -> |x| ]].|y|( ^ -> [[ |x| -> |y|, |y| -> |x| ]] )\\Big\\} \\leadsto"
+              , "\\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}"
+              , "  \\leadsto \\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |y| ( ^ -> [[ |x| -> |y|, |y| -> |x| ]] ) \\Big\\} \\leadsto"
               , "  \\leadsto \\dots"
               , "\\end{phiquation}"
               ]
@@ -759,12 +759,12 @@
           [ intercalate
               "\n"
               [ "\\begin{phiquation}"
-              , "\\Big\\{[[ @ -> [[ |x| -> [[ D> 01-, |y| -> ? ]]( |y| -> [[]] ) ]].|x| ]]\\Big\\} \\leadsto_{\\nameref{r:contextualize}}"
-              , "  \\leadsto \\Big\\{[[ |x| -> [[ D> 01-, |y| -> ? ]]( |y| -> [[]] ) ]].|x|\\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{[[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]].|x|\\Big\\} \\leadsto_{\\nameref{r:dot}}"
-              , "  \\leadsto \\Big\\{[[ D> 01-, |y| -> [[]] ]]( ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] )\\Big\\} \\leadsto_{\\nameref{r:copy}}"
-              , "  \\leadsto \\Big\\{[[ D> 01-, |y| -> [[]], ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]]\\Big\\} \\leadsto_{\\nameref{r:Mprim}}"
-              , "  \\leadsto \\Big\\{[[ D> 01-, |y| -> [[]], ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]]\\Big\\}{.}"
+              , "\\Big\\{ [[ @ -> [[ |x| -> [[ D> 01-, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| ]] \\Big\\} \\leadsto_{\\nameref{r:contextualize}}"
+              , "  \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}"
+              , "  \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]] ]] ( ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"
+              , "  \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\} \\leadsto_{\\nameref{r:Mprim}}"
+              , "  \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\}{.}"
               , "\\end{phiquation}"
               , "01-"
               ]
@@ -822,10 +822,10 @@
         [ unlines
             [ "\\begin{tabular}{rl}"
             , "\\trrule{COPY}"
-            , "  { [[ B1, \\tau -> ?, B2 ]]( \\tau -> e1 ) }"
-            , "  { [[ B1, \\tau -> e3, B2 ]] }"
-            , "  { if NF( e1 ) }"
-            , "  { where e2 <- scope( e1 ); e3 <- contextualize( e1, e2 ) }"
+            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e_1 ) }"
+            , "  { [[ B_1, \\tau -> e_3, B_2 ]] }"
+            , "  { if $ \\isnormal{ e_1 } $ }"
+            , "  { where $ e_2 \\coloneqq \\scopeof{ e_1 } $ and $ e_3 \\coloneqq \\ctx{ e_1 }{ e_2 } $ }"
             , "\\end{tabular}"
             ]
         ]
@@ -841,59 +841,59 @@
         [ unlines
             [ "\\begin{tabular}{rl}"
             , "\\trrule{ALPHA}"
-            , "  { [[ B1, \\tau1 -> ?, B2 ]]( \\tau2 -> e ) }"
-            , "  { [[ B1, \\tau1 -> ?, B2 ]]( \\tau1 -> e ) }"
-            , "  { if ordinal( \\tau2 ) = length( B1 ) }"
+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_2 -> e ) }"
+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> e ) }"
+            , "  { if $ \\indexof{ \\tau_2 } = |B_1| $ }"
             , "  { }"
             , "\\trrule{COPY}"
-            , "  { [[ B1, \\tau -> ?, B2 ]]( \\tau -> e1 ) }"
-            , "  { [[ B1, \\tau -> e3, B2 ]] }"
-            , "  { if NF( e1 ) }"
-            , "  { where e2 <- scope( e1 ); e3 <- contextualize( e1, e2 ) }"
+            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e_1 ) }"
+            , "  { [[ B_1, \\tau -> e_3, B_2 ]] }"
+            , "  { if $ \\isnormal{ e_1 } $ }"
+            , "  { where $ e_2 \\coloneqq \\scopeof{ e_1 } $ and $ e_3 \\coloneqq \\ctx{ e_1 }{ e_2 } $ }"
             , "\\trrule{DC}"
-            , "  { T( \\tau -> e ) }"
+            , "  { T ( \\tau -> e ) }"
             , "  { T }"
             , "  { }"
             , "  { }"
             , "\\trrule{DD}"
-            , "  { T.\\tau }"
+            , "  { T . \\tau }"
             , "  { T }"
             , "  { }"
             , "  { }"
             , "\\trrule{DOT}"
-            , "  { [[ B1, \\tau -> e1, B2 ]].\\tau }"
-            , "  { e2( ^ -> [[ B1, \\tau -> e1, B2 ]] ) }"
-            , "  { if NF( e1 ) }"
-            , "  { where e2 <- contextualize( e1, [[ B1, \\tau -> e1, B2 ]] ) }"
+            , "  { [[ B_1, \\tau -> e_1, B_2 ]] . \\tau }"
+            , "  { e_2 ( ^ -> [[ B_1, \\tau -> e_1, B_2 ]] ) }"
+            , "  { if $ \\isnormal{ e_1 } $ }"
+            , "  { where $ e_2 \\coloneqq \\ctx{ e_1 }{ [[ B_1, \\tau -> e_1, B_2 ]] } $ }"
             , "\\trrule{MISS}"
-            , "  { [[ B ]]( \\tau -> e ) }"
+            , "  { [[ B ]] ( \\tau -> e ) }"
             , "  { T }"
-            , "  { if \\( \\tau \\notin B \\) and \\( \\tau \\notin [ ~0, ~1, \\dots ] \\) }"
+            , "  { if $ \\tau \\notin B \\;\\text{and}\\; \\tau \\notin [ ~0, ~1, \\dots ] $ }"
             , "  { }"
             , "\\trrule{NULL}"
-            , "  { [[ B1, \\tau -> ?, B2 ]].\\tau }"
+            , "  { [[ B_1, \\tau -> ?, B_2 ]] . \\tau }"
             , "  { T }"
             , "  { }"
             , "  { }"
             , "\\trrule{OVER}"
-            , "  { [[ B1, \\tau -> e1, B2 ]]( \\tau -> e2 ) }"
+            , "  { [[ B_1, \\tau -> e_1, B_2 ]] ( \\tau -> e_2 ) }"
             , "  { T }"
-            , "  { if \\tau \\not= ^ }"
+            , "  { if $ \\tau \\not= ^ $ }"
             , "  { }"
             , "\\trrule{PHI}"
-            , "  { [[ B ]].\\tau }"
-            , "  { [[ B ]].@.\\tau }"
-            , "  { if \\( @ \\in B \\) and \\( \\tau \\notin B \\) }"
+            , "  { [[ B ]] . \\tau }"
+            , "  { [[ B ]] . @ . \\tau }"
+            , "  { if $ @ \\in B \\;\\text{and}\\; \\tau \\notin B $ }"
             , "  { }"
             , "\\trrule{STAY}"
-            , "  { [[ B1, ^ -> e1, B2 ]]( ^ -> e2 ) }"
-            , "  { [[ B1, ^ -> e1, B2 ]] }"
+            , "  { [[ B_1, ^ -> e_1, B_2 ]] ( ^ -> e_2 ) }"
+            , "  { [[ B_1, ^ -> e_1, B_2 ]] }"
             , "  { }"
             , "  { }"
             , "\\trrule{STOP}"
-            , "  { [[ B ]].\\tau }"
+            , "  { [[ B ]] . \\tau }"
             , "  { T }"
-            , "  { if \\( \\tau \\notin B \\) and \\( @ \\notin B \\) and \\( \\lambda \\notin B \\) }"
+            , "  { if $ \\tau \\notin B \\;\\text{and}\\; @ \\notin B \\;\\text{and}\\; L \\notin B $ }"
             , "  { }"
             , "\\end{tabular}"
             ]
diff --git a/test/CSTSpec.hs b/test/CSTSpec.hs
--- a/test/CSTSpec.hs
+++ b/test/CSTSpec.hs
@@ -35,7 +35,7 @@
 spec = do
   describe "builds valid CST" $
     forM_
-      [ ("Q -> Q", PR_SWEET LCB (EX_GLOBAL Φ) RCB)
+      [ ("Q -> Q", PR_SWEET LCB (EX_GLOBAL Φ) RCB NO_SPACE)
       ,
         ( "{[[ x -> Q.y ]]}"
         , PR_SWEET
@@ -44,12 +44,13 @@
                 LSB
                 EOL
                 (TAB 1)
-                (BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_DISPATCH (EX_GLOBAL Φ) (AT_LABEL "y"))) (BDS_EMPTY (TAB 1)) (TAB 1))
+                (BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_DISPATCH (EX_GLOBAL Φ) NO_SPACE (AT_LABEL "y"))) (BDS_EMPTY (TAB 1)) (TAB 1))
                 EOL
                 (TAB 0)
                 RSB
             )
             RCB
+            NO_SPACE
         )
       ]
       ( \(prog, cst) -> it prog $ do
diff --git a/test/ConditionSpec.hs b/test/ConditionSpec.hs
--- a/test/ConditionSpec.hs
+++ b/test/ConditionSpec.hs
@@ -18,7 +18,7 @@
       , " not   (in (!a1,   !B))   "
       , "alpha(x)"
       , "eq(1, 1)"
-      , "or(eq(ordinal(a),1),eq(length(!B),-2),eq(!e1,!e2),eq(!a1,x),eq(Q.org.eolang,[[ x -> 2 ]]))"
+      , "or(eq(index(a),1),eq(length(!B),-2),eq(!e1,!e2),eq(!a1,x),eq(Q.org.eolang,[[ x -> 2 ]]))"
       , "and(alpha(q),eq(-5,21))"
       , "nf([[ x -> !e ]].x)"
       , "xi(!e1)"
@@ -34,7 +34,7 @@
       , ("not(in(!a,!B))", Y.Not (Y.In (AtMeta "a") (BiMeta "B")))
       , ("alpha(y)", Y.Alpha (AtLabel "y"))
       , ("eq(1,-2)", Y.Eq (Y.CmpNum (Y.Literal 1)) (Y.CmpNum (Y.Literal (-2))))
-      , ("eq(ordinal(z),length(!B1))", Y.Eq (Y.CmpNum (Y.Ordinal (AtLabel "z"))) (Y.CmpNum (Y.Length (BiMeta "B1"))))
+      , ("eq(index(z),length(!B1))", Y.Eq (Y.CmpNum (Y.Index (AtLabel "z"))) (Y.CmpNum (Y.Length (BiMeta "B1"))))
       , ("eq(!a1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "a1")) (Y.CmpExpr (ExMeta "e2")))
       , ("or(xi(!e1), nf(Q.x))", Y.Or [Y.Xi (ExMeta "e1"), Y.NF (ExDispatch ExGlobal (AtLabel "x"))])
       , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")])