diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,11 +1,8 @@
-# Changelog for `experiments`
-
-All notable changes to this project will be documented in this file.
+# 0.2.0.0
 
-The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
-and this project adheres to the
-[Haskell Package Versioning Policy](https://pvp.haskell.org/).
+- Revised syntax of specification language.
+- Added shorthand syntax.
 
-## Unreleased
+# 0.1.0.0
 
-## 0.1.0.0 - YYYY-MM-DD
+Initial release
diff --git a/PropRatt.cabal b/PropRatt.cabal
--- a/PropRatt.cabal
+++ b/PropRatt.cabal
@@ -1,14 +1,22 @@
 cabal-version: 2.2
 name:           PropRatt
-version:        0.1.0.0
+version:        0.2.0.0
 synopsis:       Property-based testing framework for testing asynchronous FRP programs.
 category:       testing
 description:    
-                PropRatt is a property-based testing framework for testing Async Rattus programs.
+                PropRatt is a property-based testing framework for testing <https://hackage.haskell.org/package/AsyncRattus Async Rattus> programs.
                 The key component of PropRatt is its specification language, which extends basic linear temporal logic with
                 a means to express properties of several concurrent signals. This
                 allows users to express temporal properties that relate data coming from
                 different signals at different points in time.
+                .
+                More details about the specification language can be found in the <https://bahr.io/pubs/files/propratt-paper.pdf accompanying paper>.
+                .
+                Example specifications written in PropRatt:
+                .
+                * <https://github.com/pa-ba/PropRatt/blob/main/examples/timer/Timer.hs Specification for a simple GUI application>
+                .
+                * <https://github.com/pa-ba/PropRatt/blob/main/examples/main/Main.hs Specification for basic signal combinators> (@map@, @zip@, @scan@, etc.)
 author:         Christian Emil Nielsen, Mathias Faber Kristiansen, Patrick Bahr
 maintainer:     paba@itu.dk
 copyright:      2025 Christian Emil Nielsen, Mathias Faber Kristiansen, Patrick Bahr
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -2,7 +2,23 @@
 
 PropRatt is a Haskell framework for testing AsyncRattus using property-based testing.
 
+# Overview
+
+- The [main example file](examples/main/Main.hs) contains example
+  specifications that test signal combinators of the Async Rattus
+  library.
+- The [timer example file](examples/timer/Timer.hs) contains the timer
+  example from the paper.
+- The implementation of the specification language can be found in the
+  [PropRatt.LTL](src/PropRatt/LTL.hs) module.
+
+
 # Running examples
 
+Using `stack`:
 - `stack run main-example`
 - `stack run timer-example`
+
+Using `cabal`:
+- `cabal run main-example`
+- `cabal run timer-example`
diff --git a/examples/main/Main.hs b/examples/main/Main.hs
--- a/examples/main/Main.hs
+++ b/examples/main/Main.hs
@@ -1,5 +1,5 @@
 {-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
-{-# LANGUAGE TypeApplications, FlexibleInstances #-}
+{-# LANGUAGE TypeApplications, FlexibleInstances, TypeOperators #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
@@ -23,6 +23,13 @@
 
 {-# ANN module AllowLazyData #-}
 
+zipWrong :: (Stable a, Stable b) => Sig a -> Sig b -> Sig (a :* b)
+zipWrong (a ::: as) (b ::: bs) = (a :* b) ::: delay (
+        case select as bs of
+        Fst (a' ::: as') bs' -> zipWrong (a' ::: as') (b ::: bs')
+        Snd as' (b' ::: bs') -> zipWrong (a ::: as') (b ::: bs')
+        Both as' bs' -> zipWrong as' bs')
+
 filterM :: Box (a -> Bool) -> Sig a -> Sig (Maybe' a)
 filterM f (x ::: xs) = if unbox f x
   then Just' x ::: delay (filterM f (adv xs))
@@ -47,11 +54,11 @@
 prop_interleave = forAll (generateSignals @[Int, Int]) $ \intSignals ->
     let interleaved     = interleave (box (+)) (future $ first intSignals) (future $ second intSignals)
         state           = prependLater interleaved $ flatten intSignals
-        predicate       = Next $ Always $ ((Now ((Index First) |==| (Index Second)))
+        predicate       = X $ G $ ((sig1 |==| sig2)
                                         `Or`
-                                        (Now ((Index First) |==| (Index Third))))
+                                        (sig1 |==| sig3))
                                         `Or`
-                                        (Now (((Index Second) + (Index Third)) |==| (Index First)))
+                                        ((sig2 + sig3) |==| sig1)
         result          = evaluate predicate state
     in result
 
@@ -61,10 +68,7 @@
    let  jumpFunc    = box (\n -> if n > 10 then Just' (const 1) else Nothing')
         jumpSig     = jump jumpFunc (first intSignals)
         state       = prepend jumpSig $ flatten intSignals
-        predicate   = Always $
-                        Now ((Index First) |==| (Index Second))
-                        `Or`
-                        Now ((Index First) |==| (Pure 1)) --
+        predicate   = G $ (sig1 |==| sig2) `Or` (sig1 |==| pure 1)
         result      = evaluate predicate state
     in result
 
@@ -73,7 +77,7 @@
 prop_scan_failing =  forAllShrink (generateSignals @Int) shrinkHls $ \intSignals ->
     let prefixSum   = scan (box (+)) 0 (first intSignals)
         state       = prepend prefixSum $ flatten intSignals
-        predicate   = Next $ Always $ Now $ Index (Previous First) |<| (Index First)
+        predicate   = X $ G $ prev sig1 |<| sig1
         result      = evaluate predicate state
     in counterexample ("Must be natural numbers.") result
 
@@ -83,7 +87,7 @@
     let absSig      = map (box (\x -> (abs x + 1))) (first intSignals)
         prefixSum   = scan (box (+)) 0 absSig
         state       = prepend prefixSum $ flatten intSignals
-        predicate   = Next $ Always $ Now $ Index (Previous First) |<| (Index First)
+        predicate   = X $ G $ prev sig1 |<| sig1
         result      = evaluate predicate state
     in result
 
@@ -92,7 +96,7 @@
 prop_switchedSignal = forAll (generateSignals @[Int, Int]) $ \intSignals ->
     let switched    = switch (first intSignals) (future (second intSignals))
         state       = prepend switched $ flatten intSignals
-        predicate   = Until (Now ((Index First) |==| (Index Second))) (Now ((Index First) |==| (Index Third)))
+        predicate   = (sig1 |==| sig2) `U` (tick3 `And` G(sig1 |==| sig3))
         result      = evaluate predicate state
     in result
 
@@ -101,7 +105,7 @@
 prop_buffer = forAll (generateSignals @Int) $ \intSignals ->
     let bufferedSig = buffer 10 (first intSignals)
         state       = prepend bufferedSig $ flatten intSignals
-        predicate   = Next $ Always $ Now $ (Index First) |==| Index (Previous Second)
+        predicate   = X $ G $ sig1 |==| prev sig2
         result      = evaluate predicate state
     in result
 
@@ -110,7 +114,7 @@
 prop_stop = forAll (generateSignals @Int) $ \intSignals ->
     let stopped     = stop (box (>100)) (first intSignals)
         state       = prepend stopped $ flatten intSignals
-        predicate   = Always $ Implies (Now ((Index First) |>| (Pure 100))) (Always $ Next (Now (Index (Previous First) |==| (Index First))))
+        predicate   = G ((sig1 |>| pure 100) :=> (G $ X (prev sig1 |==| sig1)))
         result      = evaluate predicate state
     in result
 
@@ -119,18 +123,26 @@
 prop_zip = forAll (generateSignals @[Int, Int]) $ \intSignals ->
     let s1          = zip (first intSignals) (second intSignals)
         state       = prepend s1 $ flatten intSignals
-        predicate   = Always $ Now ((fst' <$> (Index First)) |==| (Index Second)) `And` (Now ((snd' <$> (Index First)) |==| (Index Third)))
+        predicate   = G $ ((fst' <$> sig1) |==| sig2) `And` ((snd' <$> sig1) |==| sig3)
         result      = evaluate predicate state
     in result
 
+prop_zipWrong :: Property
+prop_zipWrong = forAllShrink (generateSignals @[Int, Int]) shrinkHls $ \intSignals ->
+    let s1          = zipWrong (first intSignals) (second intSignals)
+        state       = prepend s1 $ flatten intSignals
+        predicate   = G (tick3 :=> (sig3 |==| (snd' <$> sig1)))
+        result      = evaluate predicate state
+    in counterexample (show state) result
+
 prop_filter :: Property
 prop_filter = forAll (generateSignals @Int) $ \intSignals ->
   let filtered      = filterM (box (>= 10)) (first intSignals)
       state         = prepend filtered $ flatten intSignals
-      predicate     = Always $ 
-            Implies (Now ((Index Second) |>=| Pure (10))) (Now ((Index First) |>=| (Pure (Just' 10))))
+      predicate     = G $
+            ((sig2 |>=| pure 10) :=> (sig1 |>=| pure (Just' 10)))
             `And`
-            Implies (Now ((Index Second) |<| Pure (10))) (Now ((Index First) |==| (Pure Nothing')))
+            (sig2 |<| pure 10) :=> (sig1 |==| pure Nothing')
       result        = evaluate predicate state
   in result
 
@@ -138,8 +150,9 @@
 prop_triggerM = forAll (generateSignals @[Int, Int]) $ \intSignals ->
   let triggered     = triggerM (box (*)) (first intSignals) (second intSignals)
       state         = prepend triggered $ flatten intSignals
-      predicate     = Always $ 
-            Implies (Now ((Ticked Second) |==| (Pure True))) ((Now ((Ticked First) |==| (Pure True))) `And` (Now ((fromMaybe' 0 <$> (Index First)) |==| ((Index Second) * (Index Third)))))
+      predicate     = G 
+            tick2 :=> 
+            (tick1 `And` ((fromMaybe' 0 <$> sig1) |==| (sig2 * sig3)))
       result        = evaluate predicate state
   in result
 
@@ -147,10 +160,7 @@
 prop_parallel = forAllShrink (generateSignals @[Int, Int]) shrinkHls $ \intSignals ->
     let paralleled  = parallel (first intSignals) (second intSignals)
         state       = prepend paralleled $ flatten intSignals
-        predicate   = Always $
-            Implies (Now (Ticked Third)) (Now (Ticked First))
-            `And`
-            Implies (Now (Ticked Second)) (Now (Ticked First))
+        predicate   = G $ (tick3 :=> tick1) `And`(tick2 :=> tick1)
         result      = evaluate predicate state
     in result
 
@@ -158,10 +168,10 @@
 prop_isStuttering = forAll (generateSignals @[Int, Int]) $ \intSignals ->
     let stuttered   = stutter (first intSignals) (second intSignals)
         state       = prepend stuttered $ flatten intSignals
-        predicate   = Always $
-            Implies (Now (Ticked First)) (Now (Index First |==| Index Second))
+        predicate   = G $
+            (tick1 :=> (sig1 |==| sig2))
             `And`
-            Next (Implies (And (Now (Ticked Third)) (Not (Now (Ticked Second)))) (Now (Index (Previous First) |==| Index First)))
+            X ((tick3 `And` Not (tick2)) :=> (prev sig1 |==| sig1))
         result      = evaluate predicate state
     in result
 
@@ -169,14 +179,14 @@
 prop_functionIsMonotonic = forAll (generateSignals @Int) $ \intSignals ->
     let mono        = monotonic (first intSignals)
         state       = singletonH mono
-        predicate   = Always $ Next (Now ((Index First) |>=| (Index (Previous First))))
+        predicate   = G $ X (sig1 |>=| prev sig1)
         result      = evaluate predicate state
     in result
 
 prop_singleSignalAlwaysTicks :: Property
 prop_singleSignalAlwaysTicks = forAllShrink (arbitrary :: Gen (Sig Int)) shrink $ \sig ->
     let state       = singletonH sig
-        predicate   = Always $ Now ((Ticked First) |==| (Pure True))
+        predicate   = G tick1
         result      = evaluate predicate state
     in result
 
@@ -187,14 +197,11 @@
         (_ ::: ys)          = (scan (box (\n _ -> n + 1)) 0 (takeN (sigLength xs) mkSigZero)) :: Sig Int
         zs                  = switchR xs (mapAwait (box (\b _ -> const b)) ys)
         state               = prepend zs $ prependLater ys $ flatten intSignals
-        predicate           = (Now ((Index First) |==| (Index Third)))
-                                `Until`
-                                (Now ((Ticked Second) |==| (Pure True)))
+        predicate           = ((sig1 |==| sig3) `U`tick2)
                                 `And` 
-                                ((Always $ Next 
-                                    (((Implies  (Not (Now (Ticked Second))) (Now ((Index (Previous First)) |==| (Index First))))))))
-                                `Until`
-                               (Next $ (Implies (Now (Ticked Second)) (Not (Now ((Index (Previous First)) |==| (Index First))))))
+                                (G $ X (Not tick2 :=> (prev sig1 |==| sig1)))
+                                `U`
+                                 (X (tick2 :=> Not (prev sig1 |==| sig1)))
         result              = evaluate predicate state
     in counterexample (show state) result
 
@@ -205,21 +212,19 @@
         ggg                 = Delay (IntSet.fromList [1,2,3]) (\_ a -> const a)
         zs                  = switchS xs ggg
         state               = prepend zs $ prependLater ys $ flatten intSignals
-        predicate           =(Now ((Index First) |==| (Index Third)))
-                                `Until`
-                                (Now ((Ticked Second) |==| (Pure True)))
+        predicate           =(sig1 |==| sig3)
+                                `U`
+                                tick2
                                 `And` 
-                                ((Always $ Next 
-                                    (((Implies  (Not (Now (Ticked Second))) (Now ((Index (Previous First)) |==| (Index First))))))))
-                                `Until`
-                               (Next $ (Implies (Now (Ticked Second)) (Not (Now ((Index (Previous First)) |==| (Index First))))))
+                                (G $ X (Not tick2 :=> (prev sig1 |==| sig1)))
+                                `U`(X (tick2 :=> Not (prev sig1 |==| sig1)))
         result              = evaluate predicate state
     in counterexample (show gg ++ show zs ++ show xs) result
 
 prop_sigLength :: Property
 prop_sigLength = forAllShrink (arbitrary :: Gen (Sig Int)) shrink $ \(sig :: Sig Int) ->
         let state       = singletonH (sig :: Sig Int)
-            predicate   = Always $ (Now ((Index First) |<| (Pure 50)))
+            predicate   = G (sig1 |<| pure 50)
             result      = evaluate predicate state
         in result
 
@@ -227,14 +232,14 @@
 prop_sigIsPositive = forAll (generateSignals @Int) $ \sig ->
         let mapped      = map (box (abs)) (first sig)
             state       = singletonH mapped
-            predicate   = Next $ Always $ Now ((Index (Prior 1 First)) |>=| (Pure 0))
+            predicate   = X $ G (prevN 1 sig1 |>=| pure 0)
             result      = evaluate predicate state 
         in result
 
 prop_catchsubtle :: Property
 prop_catchsubtle = forAllShrink (arbitrary :: Gen (Sig Int)) shrink $ \(sig :: Sig Int) ->
         let state       = singletonH (sig :: Sig Int)
-            predicate   = Always $ Implies (Now ((Index First) |>| (Pure 80))) (Next $ (Now ((Index First) |<| (Index (Previous First)))))
+            predicate   = G ((sig1 |>| pure 80) :=> X (sig1 |<| (prev sig1)))
             result      = evaluate predicate state
         in result
 
@@ -242,7 +247,7 @@
 prop_predLengthOutsideDefault =  forAllShrink (generateSignals @Int) shrinkHls $ \intSignals ->
     let prefixSum   = scan (box (+)) 0 (first intSignals)
         state       = prepend prefixSum $ flatten intSignals
-        predicate   = After 100 $ Always $ Now $ Index (Previous First) |<| (Index First)
+        predicate   = XN 100 $ G (prev sig1 |<| sig1)
         result      = evaluate predicate state
     in result
 
@@ -274,3 +279,5 @@
     quickCheck (withMaxSuccess 1000 prop_catchsubtle)
     putStrLn "====================="
     quickCheck prop_predLengthOutsideDefault
+    putStrLn "====================="
+    quickCheck prop_zipWrong
diff --git a/examples/timer/Timer.hs b/examples/timer/Timer.hs
--- a/examples/timer/Timer.hs
+++ b/examples/timer/Timer.hs
@@ -17,10 +17,15 @@
 
 {-# ANN module AllowLazyData #-}
 
-{-# ANN everySecondSig AllowRecursion #-}
-everySecondSig :: O (Sig ())
-everySecondSig = Delay (IntSet.fromList [2]) (\_ -> () ::: everySecondSig)
+{-# ANN everySig2Sig' AllowRecursion #-}
+everySig2Sig' :: Int -> O (Sig ())
+everySig2Sig' 0 = never
+everySig2Sig' n = Delay (IntSet.fromList [2]) (\_ -> () ::: everySig2Sig' (n-1))
 
+everySig2Sig :: O (Sig ())
+everySig2Sig = everySig2Sig' 100
+
+
 nats :: O (Sig ()) -> (Int :* Int) -> Sig (Int :* Int)
 nats later (n :* max) = stop
     (box (\ (n' :* max') -> n' >= max'))
@@ -38,15 +43,15 @@
             currentMax  = current sliderSig
             setMaxSig   = mapAwait (box setMax) ss
             inputSig    = interleave (box (.)) resetSig setMaxSig
-            inputSig'   = mapAwait (box ((nats everySecondSig) .)) inputSig
-            counterSig  = switchR ((nats everySecondSig) (0 :* currentMax)) inputSig'
+            inputSig'   = mapAwait (box ((nats everySig2Sig) .)) inputSig
+            counterSig  = switchR ((nats everySig2Sig) (0 :* currentMax)) inputSig'
     in counterSig
 
 prop_counterSigAlwaysLessThanMax :: Property
 prop_counterSigAlwaysLessThanMax = forAll genDouble $ \(reset, slider) ->
         let counterSig  = timerState reset slider
             state       = prepend counterSig $ prepend reset $ singletonH slider
-            predicate   = Always $ Now ((fst' <$> Index First) |<=| (snd' <$> Index First))
+            predicate   = G ((fst' <$> sig1) |<=| (snd' <$> sig1))
             result      = evaluate predicate state
         in counterexample (show state) result
   where
@@ -59,7 +64,7 @@
 prop_maxAlwaysEqualsMax = forAll genDouble $ \(reset, slider) ->
         let counterSig  = timerState reset slider
             state       = prepend counterSig $ prepend reset $ singletonH slider
-            predicate   = Always $ Now ((Index Third) |==| (snd' <$> Index First))
+            predicate   = G (sig3 |==| (snd' <$> sig1))
             result      = evaluate predicate state
         in counterexample (show state) result
   where
@@ -73,11 +78,11 @@
 prop_concurrentResetAndSlider = forAll genDouble $ \(reset, slider) ->
         let counterSig  = timerState reset slider
             state       = prepend counterSig $ prepend reset $ singletonH slider
-            predicate   = Always $ Implies
-                (And (Now ((Ticked Second))) (Now ((Ticked Third))))
-                ((Now (((Index Third)) |==| (snd' <$> Index First)))
+            predicate   = G $ 
+                ((tick2 `And` tick3) :=>
+                ((sig3 |==| (snd' <$> sig1))
                 `And`
-                (Now ((Pure 0) |==| (fst' <$> Index First))))
+                (pure 0 |==| (fst' <$> sig1))))
             result      = evaluate predicate state
         in counterexample (show state) result
   where
@@ -86,14 +91,41 @@
       reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))
       return (reset, slider)
 
+
+
+prop_reset :: Property
+prop_reset = forAll genDouble $ \(reset, slider) ->
+        let counterSig  = timerState reset slider
+            state       = prepend counterSig $ prepend reset $ singletonH slider
+            predicate   = G (tick2 :=> (pure 0 |==| (fst' <$> sig1)))
+            result      = evaluate predicate state
+        in counterexample (show state) result
+  where
+    genDouble = do
+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))
+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))
+      return (reset, slider)
+
+prop_max :: Property
+prop_max = forAll genDouble $ \(reset, slider) ->
+        let counterSig  = timerState reset slider
+            state       = prepend counterSig $ prepend reset $ singletonH slider
+            predicate   = G (sig3 |==| (snd' <$> sig1))
+            result      = evaluate predicate state
+        in counterexample (show state) result
+  where
+    genDouble = do
+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))
+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))
+      return (reset, slider)
+
 prop_timerIsStrictlyMonotonicallyIncreasing :: Property
 prop_timerIsStrictlyMonotonicallyIncreasing = forAll genDouble $ \(reset, slider) ->
         let counterSig  = timerState reset slider
             state       = prepend counterSig $ prepend reset $ singletonH slider
-            predicate   = Always $ Next $
-                Implies
-                ((Now (Ticked First)) `And` ((Not (Now (Ticked Second)) `And` (Not (Now (Ticked Third))))))
-                (Now (((fst' <$> (Index First)) |>| (fst' <$> (Index (Previous First))))))
+            predicate   = G $ X
+                ((tick1 `And` (Not tick2 `And` Not tick3)) :=>
+                ((fst' <$> sig1) |>| (fst' <$> prev sig1)))
             result      = evaluate predicate state
         in counterexample (show state) result
   where
@@ -107,7 +139,7 @@
 prop_init = forAll genDouble $ \(reset, slider) ->
         let counterSig  = timerState reset slider
             state       = prepend counterSig $ prepend reset $ singletonH slider
-            predicate   = Now ((fst' <$> (Index First)) |==| (Pure 0)) `And` (Now ((snd' <$> (Index First)) |==| (Index Third)))
+            predicate   = ((fst' <$> sig1) |==| pure 0) `And` ((snd' <$> sig1) |==| sig3)
             result      = evaluate predicate state
         in counterexample (show state) result
   where
@@ -121,12 +153,11 @@
 prop_counterSigStaysAtMaxValue = forAllShrink genDouble shrink $ \(reset, slider) ->
         let counterSig  = timerState reset slider
             state       = prepend counterSig $ prepend reset $ singletonH slider
-            predicate   = Always $
-                Implies
-                    (Now ((fst' <$> (Index First)) |==| (snd' <$> (Index First))))
-                    (Next $ (Now ((fst' <$> (Index First)) |==| (fst' <$> (Index (Previous First))))
-                    `Until`
-                    ((Now (Ticked Second)) `Or` (Now (Ticked Third)))))
+            predicate   = G $
+                    (((fst' <$> sig1) |==| (snd' <$> sig1)) :=>
+                    (X $ ((fst' <$> sig1) |==| (fst' <$> prev sig1))
+                    `U`
+                    (tick2 `Or` tick3)))
             result      = evaluate predicate state
         in counterexample (show state) result
   where
@@ -139,7 +170,7 @@
 prop_counterSigAlwaysTicks = forAll genDouble $ \(reset, slider) ->
         let counterSig  = timerState reset slider
             state       = prepend counterSig $ prepend reset $ singletonH slider
-            predicate   = Always $ Now (Ticked First) `And` (Next $ Now (Ticked First))
+            predicate   = G (tick1 `And` X tick1)
             result      = evaluate predicate state
         in counterexample (show state) result
   where
@@ -148,6 +179,38 @@
       reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))
       return (reset, slider)
 
+
+
+-- the timer is constant unless a second passes or reset is pressed
+prop_timerConst :: Property
+prop_timerConst = forAllShrink genDouble shrink $ \(reset, slider) ->
+        let counterSig  = timerState reset slider
+            state       = prepend counterSig $ prepend reset $ prepend slider $ singletonH (() ::: everySig2Sig)
+            predicate   = G (X ((Not tick2 `And` Not tick4) :=> ((fst' <$> prev sig1) |==| (fst' <$> sig1))))
+            result      = evaluate predicate state
+        in counterexample (show state) result
+  where
+    genDouble = do
+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))
+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig ()))
+      return (reset, slider)
+
+
+
+-- the timer ticks unless it reached its maximum
+prop_timerTicks :: Property
+prop_timerTicks = forAllShrink genDouble shrink $ \(reset, slider) ->
+        let counterSig  = timerState reset slider
+            state       = prepend counterSig $ prepend reset $ prepend slider $ singletonH (() ::: everySig2Sig)
+            predicate   = G ( ((snd' <$> sig1) |<| sig3 `And` X tick4)  :=> X ((snd' <$> sig1) |==| ((+1) . snd' <$> prev sig1)))
+            result      = evaluate predicate state
+        in counterexample (show state) result
+  where
+    genDouble = do
+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))
+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig ()))
+      return (reset, slider)
+
 main :: IO ()
 main = do
     quickCheck prop_counterSigAlwaysLessThanMax
@@ -157,3 +220,7 @@
     quickCheck prop_init
     quickCheck prop_counterSigStaysAtMaxValue
     quickCheck prop_counterSigAlwaysTicks
+    quickCheck prop_reset
+    quickCheck prop_max
+    quickCheck prop_timerConst
+    quickCheck prop_timerTicks
diff --git a/src/PropRatt/Arbitrary.hs b/src/PropRatt/Arbitrary.hs
--- a/src/PropRatt/Arbitrary.hs
+++ b/src/PropRatt/Arbitrary.hs
@@ -103,14 +103,17 @@
 genClockChannelWeighted :: Gen Int
 genClockChannelWeighted = frequency [(1, pure 1), (1, pure 2), (50, pure 3)]
 
-genClock :: Int -> Gen Clock
-genClock n = case n of
+
+genClock :: Gen Clock
+genClock = do
+  n <- chooseInt (1, 3)
+  case n of
     1 -> do
       x <- chooseInt (1,3)
       return (IntSet.fromList [x])
-    2 -> frequency [(1, return (IntSet.fromList [1,2])),(1, return (IntSet.fromList [2,3])),(1, return (IntSet.fromList [1,3]))]
+    2 -> elements $ map IntSet.fromList [[1,2], [2,3], [1,3]]
     3 -> return (IntSet.fromList [1,2,3])
-    _ -> error "Partial function doesnt support n > 3"
+    _ -> error "genClock: impossible!"
 
 genClockListWeighted :: Gen [Int]
 genClockListWeighted = vectorOf 1 genClockChannelWeighted
@@ -128,8 +131,7 @@
           return (x ::: never)
         go m = do
           x <- arbitrary
-          len <- chooseInt (1, 3)
-          cl <- genClock len
+          cl <- genClock
           xs <- go (m - 1)
           let later = Delay cl (\_ -> xs)
           return (x ::: later)
@@ -147,8 +149,7 @@
           return (x ::: never)
         go m = do
           x <- gen
-          len <- chooseInt (1, 3)
-          cl <- genClock len
+          cl <- genClock
           xs <- go (m - 1)
           let later = Delay cl (\_ -> xs)
           return (x ::: later)
@@ -190,7 +191,7 @@
   generateHList = do
     x <- arbitrary
     xs <- generateHList @ts
-    return (x %: xs)
+    return (x :% xs)
 
 generateSignals :: forall a. HListGen (ToList a) => Gen (HList (Map Sig (ToList a)))
 generateSignals = generateHList @(ToList a)
@@ -202,7 +203,7 @@
   shrinkHls _ = []
 
 instance (Arbitrary a, ShrinkHList as) => ShrinkHList (a ': as) where
-  shrinkHls (HCons x xs) =
-    [ HCons x' xs | x'  <- shrink x ] ++
-    [ HCons x xs' | xs' <- shrinkHls xs ] ++
-    [ HCons x' xs' | x'  <- shrink x, xs' <- shrinkHls xs ]
+  shrinkHls (x :% xs) =
+    [ x' :% xs | x'  <- shrink x ] ++
+    [ x :% xs' | xs' <- shrinkHls xs ] ++
+    [ x' :% xs' | x'  <- shrink x, xs' <- shrinkHls xs ]
diff --git a/src/PropRatt/Core.hs b/src/PropRatt/Core.hs
--- a/src/PropRatt/Core.hs
+++ b/src/PropRatt/Core.hs
@@ -40,7 +40,7 @@
 
 instance (Stable a, Stable (Value a), Flatten as bs, Falsify bs) => Flatten (Sig a ': as) (Value a ': bs) where
   flatten :: HList (Sig a : as) -> Sig (HList (Value a : bs))
-  flatten (HCons h t) = prepend h (flatten t)
+  flatten (h :% t) = prepend h (flatten t)
 
 class Falsify ts where
   toFalse :: HList ts -> HList ts
@@ -51,24 +51,24 @@
 
 instance (Falsify ts) => Falsify (Value t ': ts) where
   toFalse :: HList (Value t : ts) -> HList (Value t : ts)
-  toFalse (HCons (Current _ x) t) = Current (HasTicked False) x %: toFalse t
+  toFalse (Current _ x :% t) = Current (HasTick False) x :% toFalse t
 
 -- | Like 'prepend', but the new head is delayed by one tick.
 --   This emits a dummy value at the head on the first tick, then behaves like 'prepend' on subsequent ticks.
 prependLater :: (Stable t, Stable (HList ts), Falsify ts) => O (Sig t) -> Sig (HList ts) -> Sig (HList (Value t ': ts))
 prependLater xs (y ::: ys) =
-  HCons (Current (HasTicked False) Nil) y ::: prependAwait Nil xs y ys
+  (Current (HasTick False) Nil :% y) ::: prependAwait Nil xs y ys
 
 prepend :: (Stable t, Stable (HList ts), Falsify ts) => Sig t -> Sig (HList ts) -> Sig (HList (Value t ': ts))
 prepend (x ::: xs) (y ::: ys) =
-  HCons (Current (HasTicked True) (x :! Nil)) y ::: prependAwait (x :! Nil) xs y ys
+  (Current (HasTick True) (x :! Nil) :% y) ::: prependAwait (x :! Nil) xs y ys
 
 prependAwait :: (Stable t, Stable hls, hls ~ HList ts, Falsify ts) => List t -> O (Sig t) -> hls -> O (Sig hls) -> O (Sig (HList (Value t ': ts)))
 prependAwait x xs y ys  = delay (
   case select xs ys of
-     Fst (x' ::: xs')   ys'         -> (Current (HasTicked True) (x' :! x) %: toFalse y)  ::: prependAwait (x' :! x) xs' y ys'
-     Snd xs' (y' ::: ys')           -> (Current (HasTicked False) x %: y')                ::: prependAwait x xs' y' ys'
-     Both (x' ::: xs') (y' ::: ys') -> (Current (HasTicked True) (x' :! x) %: y')         ::: prependAwait (x' :! x) xs' y' ys')
+     Fst (x' ::: xs')   ys'         -> (Current (HasTick True) (x' :! x) :% toFalse y)  ::: prependAwait (x' :! x) xs' y ys'
+     Snd xs' (y' ::: ys')           -> (Current (HasTick False) x :% y')                ::: prependAwait x xs' y' ys'
+     Both (x' ::: xs') (y' ::: ys') -> (Current (HasTick True) (x' :! x) :% y')         ::: prependAwait (x' :! x) xs' y' ys')
 
 singletonH :: (Stable t) => Sig t -> Sig (HList '[Value t])
-singletonH sig = flatten (sig %: HNil)
+singletonH sig = flatten (sig :% HNil)
diff --git a/src/PropRatt/HList.hs b/src/PropRatt/HList.hs
--- a/src/PropRatt/HList.hs
+++ b/src/PropRatt/HList.hs
@@ -13,57 +13,55 @@
 {-# OPTIONS_GHC -Wno-partial-type-signatures #-}
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
 
-module PropRatt.HList (HList(..), (%:), first,second,third,fourth,fifth,sixth,seventh,eighth,ninth,lengthH) where       
+module PropRatt.HList (HList(..), first,second,third,fourth,fifth,sixth,seventh,eighth,ninth,lengthH) where       
 import AsyncRattus.InternalPrimitives ( Stable )
 import Data.Kind (Type)
 
 data HList :: [Type] -> Type where
   HNil :: HList '[]
-  HCons :: !x -> !(HList xs) -> HList (x ': xs)
+  (:%) :: !x -> !(HList xs) -> HList (x ': xs)
 
-infixr 5 %:
-(%:) :: x -> HList xs -> HList (x ': xs)
-(%:) = HCons
+infixr 5 :%
 
 instance Show (HList '[]) where
   show :: HList '[] -> String
-  show HNil = "HNil"
+  show HNil = "\n"
 
 instance (Show x, (Show (HList xs))) => Show (HList (x ': xs)) where
   show :: (Show x, Show (HList xs)) => HList (x : xs) -> String
-  show (HCons x xs) = show x ++ " %: " ++ show xs
+  show (x :% xs) = show x ++ "; " ++ show xs
 
 instance Stable (HList '[]) where
 instance (Stable a, Stable (HList as)) => Stable (HList (a ': as)) where
 
 first :: HList (a ': _) -> a
-first (HCons h _) = h
+first (v :% _) = v
 
 second :: HList (_ ': a ': _) -> a
-second (HCons _ (HCons h2 _)) = h2
+second (_ :% v :% _) = v
 
 third :: HList (_ ': _ ': a ': _) -> a
-third (HCons _ (HCons _ (HCons h3 _))) = h3
+third (_ :% _ :% v :% _) = v
 
 fourth :: HList (_ ': _ ': _ ': a ': _) -> a
-fourth (HCons _ (HCons _ (HCons _ (HCons h4 _)))) = h4
+fourth (_ :% _ :% _ :% v :% _) = v
 
 fifth :: HList (_ ': _ ': _ ': _ ': a ': _) -> a
-fifth (HCons _ (HCons _ (HCons _ (HCons _ (HCons h5 _))))) = h5
+fifth (_ :% _ :% _ :% _ :% v :% _) = v
 
 sixth :: HList (_ ': _ ': _ ': _ ': _ ': a ': _) -> a
-sixth (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h6 _)))))) = h6
+sixth (_ :% _ :% _ :% _ :% _ :% v :% _) = v
 
 seventh :: HList (_ ':_ ': _ ': _ ': _ ': _ ': a ': _) -> a
-seventh (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h7 _))))))) = h7
+seventh (_ :% _ :% _ :% _ :% _ :% _ :% v :% _) = v
 
 eighth :: HList (_ ': _ ': _ ': _ ': _ ': _ ': _ ': a ': _) -> a
-eighth (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h8 _)))))))) = h8
+eighth (_ :% _ :% _ :% _ :% _ :% _ :% _ :% v :% _) = v
 
 ninth :: HList (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': a ': _) -> a
-ninth (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h9 _))))))))) = h9
+ninth (_ :% _ :% _ :% _ :% _ :% _ :% _ :% _ :% v :% _) = v
 
 
 lengthH :: HList ts -> Int -> Int
 lengthH HNil n = n
-lengthH (HCons _ as) n = lengthH as (n+1)
+lengthH (_ :% as) n = lengthH as (n+1)
diff --git a/src/PropRatt/LTL.hs b/src/PropRatt/LTL.hs
--- a/src/PropRatt/LTL.hs
+++ b/src/PropRatt/LTL.hs
@@ -19,6 +19,9 @@
     (|>|),
     (|>=|),
     (|==|),
+    tick1,tick2,tick3,tick4,
+    sig1,sig2,sig3,sig4,
+    prev, prevN
   )
 where
 
@@ -32,53 +35,52 @@
 import PropRatt.Utils
 
 data Pred (ts :: [Type]) where
-  Tautology     :: Pred ts
-  Contradiction :: Pred ts
-  Now           :: Expr ts Bool -> Pred ts
-  Not           :: Pred ts -> Pred ts
-  And           :: Pred ts -> Pred ts -> Pred ts
-  Or            :: Pred ts -> Pred ts -> Pred ts
-  Until         :: Pred ts -> Pred ts -> Pred ts
-  Next          :: Pred ts -> Pred ts
-  Implies       :: Pred ts -> Pred ts -> Pred ts
-  Always        :: Pred ts -> Pred ts
-  Eventually    :: Pred ts -> Pred ts
-  After         :: Int -> Pred ts-> Pred ts
-  Release       :: Pred ts -> Pred ts -> Pred ts
+  TT    :: Pred ts
+  FF    :: Pred ts
+  Now   :: Expr ts Bool -> Pred ts
+  Not   :: Pred ts -> Pred ts
+  And   :: Pred ts -> Pred ts -> Pred ts
+  Or    :: Pred ts -> Pred ts -> Pred ts
+  U     :: Pred ts -> Pred ts -> Pred ts
+  X     :: Pred ts -> Pred ts
+  (:=>) :: Pred ts -> Pred ts -> Pred ts
+  G     :: Pred ts -> Pred ts
+  F     :: Pred ts -> Pred ts
+  XN    :: Int -> Pred ts-> Pred ts
+  R     :: Pred ts -> Pred ts -> Pred ts
 
 data Expr (ts :: [Type]) (t :: Type) where
-  Pure    :: t -> Expr ts t
-  Apply   :: Expr ts (t -> r) -> Expr ts t -> Expr ts r
-  Index   :: Lookup ts t -> Expr ts t
-  Ticked  :: Lookup ts t -> Expr ts Bool
+  Pure  :: t -> Expr ts t
+  App   :: Expr ts (t -> r) -> Expr ts t -> Expr ts r
+  Val   :: Lookup ts t -> Expr ts t
+  Tick  :: Lookup ts t -> Expr ts Bool
 
 data Lookup (ts :: [Type]) (t :: Type) where
-  Previous  :: Lookup ts t -> Lookup ts t
-  Prior     :: Int -> Lookup ts t -> Lookup ts t
-  First     :: Lookup (Value t ': x) t
-  Second    :: Lookup (x1 ': Value t ': x2) t
-  Third     :: Lookup (x1 ': x2 ': Value t ': x3) t
-  Fourth    :: Lookup (x1 ': x2 ': x3 ': Value t ': x4) t
-  Fifth     :: Lookup (x1 ': x2 ': x3 ': x4 ': Value t ': x5) t
-  Sixth     :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': Value t ': x6) t
-  Seventh   :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': Value t ': x7) t
-  Eighth    :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': x7 ': Value t ': x8) t
-  Ninth     :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': x7 ': x8 ': Value t ': x9) t
+  Prev   :: Lookup ts t -> Lookup ts t
+  PrevN  :: Int -> Lookup ts t -> Lookup ts t
+  Sig1   :: Lookup (Value t ': x) t
+  Sig2   :: Lookup (x1 ': Value t ': x2) t
+  Sig3   :: Lookup (x1 ': x2 ': Value t ': x3) t
+  Sig4   :: Lookup (x1 ': x2 ': x3 ': Value t ': x4) t
+  Sig5   :: Lookup (x1 ': x2 ': x3 ': x4 ': Value t ': x5) t
+  Sig6   :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': Value t ': x6) t
+  Sig7   :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': Value t ': x7) t
+  Sig8   :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': x7 ': Value t ': x8) t
+  Sig9   :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': x7 ': x8 ': Value t ': x9) t
 
 instance Functor (Expr ts) where
   fmap :: (t -> r) -> Expr ts t -> Expr ts r
   fmap f (Pure x)     = Pure (f x)
-  fmap f (Apply g x)  = Apply (fmap (f .) g) x
-  fmap f (Index lu)   = Apply (Pure f) (Index lu)
-  fmap f (Ticked lu)  = Apply (Pure f) (Ticked lu)
+  fmap f (App g x)  = App (fmap (f .) g) x
+  fmap f (Val lu)   = App (Pure f) (Val lu)
+  fmap f (Tick lu)  = App (Pure f) (Tick lu)
 
 instance Applicative (Expr ts) where
     pure :: t -> Expr ts t
     pure = Pure
     (<*>) :: Expr ts (t -> r) -> Expr ts t -> Expr ts r
     Pure f <*> x = fmap f x
-    Apply f g <*> x = Apply (Apply f g) x
-    (<*>) _ _ = error "Expr: unsupported constructor for applicative application."
+    f <*> x = App f x
 
 instance Num t => Num (Expr ts t) where
   (+) :: Expr ts t -> Expr ts t -> Expr ts t
@@ -96,41 +98,78 @@
   fromInteger :: Integer -> Expr ts t
   fromInteger n = pure (fromInteger n)
 
-(|<|) :: (Applicative f, Ord t) => f t -> f t -> f Bool
-x |<| y = (<) <$> x <*> y
-(|<=|) :: (Applicative f, Ord t) => f t -> f t -> f Bool
-x |<=| y = (<=) <$> x <*> y
-(|>|) :: (Applicative f, Ord t) => f t -> f t -> f Bool
-x |>| y = (>) <$> x <*> y
-(|>=|) :: (Applicative f, Ord t) => f t -> f t -> f Bool
-x |>=| y = (>=) <$> x <*> y
-(|==|) :: (Applicative f, Eq t) => f t -> f t -> f Bool
-x |==| y = (==) <$> x <*> y
+(|<|) :: Ord t => Expr ts t -> Expr ts t -> Pred ts
+x |<| y = Now ((<) <$> x <*> y)
+(|<=|) :: Ord t => Expr ts t -> Expr ts t -> Pred ts
+x |<=| y = Now ((<=) <$> x <*> y)
+(|>|) :: Ord t => Expr ts t -> Expr ts t -> Pred ts
+x |>| y = Now ((>) <$> x <*> y)
+(|>=|) :: Ord t => Expr ts t -> Expr ts t -> Pred ts
+x |>=| y = Now ((>=) <$> x <*> y)
+(|==|) :: Ord t => Expr ts t -> Expr ts t -> Pred ts
+x |==| y = Now ((==) <$> x <*> y)
 
--- | Checks whether the instances of "previous" is within scope of t "next" operator.
+tick1 :: Pred (Value t ': ts)
+tick1 = Now (Tick Sig1)
+
+tick2 :: Pred (t1 ': Value t2 ': ts)
+tick2 = Now (Tick Sig2)
+
+tick3 :: Pred (t1 ': t2 ': Value t3 ': ts)
+tick3 = Now (Tick Sig3)
+
+tick4 :: Pred (t1 ': t2 ': t3 ': Value t4 ': ts)
+tick4 = Now (Tick Sig4)
+
+
+sig1 :: Expr (Value t ': ts) t
+sig1 = Val Sig1
+
+sig2 :: Expr (t1 ': Value t2 ': ts) t2
+sig2 = Val Sig2
+
+sig3 :: Expr (t1 ': t2 ': Value t3 ': ts) t3
+sig3 = Val Sig3
+
+sig4 :: Expr (t1 ': t2 ': t3 ': Value t4 ': ts) t4
+sig4 = Val Sig4
+
+prev :: Expr ts t -> Expr ts t
+prev (Pure x)   = Pure x
+prev (App f x)  = App (prev f) (prev x)
+prev (Val lu)   = Val (Prev lu)
+prev (Tick lu)  = Tick (Prev lu)
+
+prevN :: Int -> Expr ts t -> Expr ts t
+prevN _ (Pure x)   = Pure x
+prevN n (App f x)  = App (prevN n f) (prevN n x)
+prevN n (Val lu)   = Val (PrevN n lu)
+prevN n (Tick lu)  = Tick (PrevN n lu)
+
+-- | Checks whether the instances of "previous" is within scope of t "X" operator.
 -- This prevents the evaluation from looking too far back in time.
 checkScope :: Pred ts -> Bool
 checkScope p = checkPred p 0
 
 -- | Traverses the predicate supplied and exits early if it finds a subtree where the scope is negative.
--- The scope is incremented for each next constructor, and decremented for each previous or prior constructor.
+-- The scope is incremented for each X constructor, and decremented for each previous or prior constructor.
 checkPred :: Pred ts -> Int -> Bool
 checkPred predicate scope =
   valid scope &&
   case predicate of
-    Tautology       -> valid scope
-    Contradiction   -> valid scope
-    Now expr        -> valid (checkExpr expr scope)
-    Not p           -> checkPred p scope
-    And p1 p2       -> checkPred p1 scope && checkPred p2 scope
-    Or p1 p2        -> checkPred p1 scope || checkPred p2 scope
-    Until p1 p2     -> checkPred p1 scope && checkPred p2 scope
-    Next p          -> checkPred p (scope + 1)
-    Implies p1 p2   -> checkPred p1 scope && checkPred p2 scope
-    Release p1 p2   -> checkPred p1 scope && checkPred p2 scope
-    Always p        -> checkPred p scope
-    Eventually p    -> checkPred p scope
-    After n p       -> checkPred p (scope + n)
+    TT        -> valid scope
+    FF        -> valid scope
+    Now expr  -> valid (checkExpr expr scope)
+    Not p     -> checkPred p scope
+    And p1 p2 -> checkPred p1 scope && checkPred p2 scope
+    Or p1 p2  -> checkPred p1 scope || checkPred p2 scope
+    U p1 p2   -> checkPred p1 scope && checkPred p2 scope
+    X p       -> checkPred p (scope + 1)
+    p1 :=> p2 -> checkPred p1 scope && checkPred p2 scope
+    R p1 p2   -> checkPred p1 scope && checkPred p2 scope
+    G p       -> checkPred p scope
+    F p       -> checkPred p scope
+    XN n p    -> checkPred p (scope + n)
   where
     valid s = s >= 0
 
@@ -138,111 +177,111 @@
 checkExpr :: Expr ts t -> Int -> Int
 checkExpr expr scope =
   case expr of
-    Pure _        -> scope
-    Apply fun arg -> min (checkExpr fun scope) (checkExpr arg scope)
-    Index lu      -> checkLookup lu scope
-    Ticked lu     -> checkLookup lu scope
+    Pure _      -> scope
+    App fun arg -> min (checkExpr fun scope) (checkExpr arg scope)
+    Val lu      -> checkLookup lu scope
+    Tick lu     -> checkLookup lu scope
 
 checkLookup :: Lookup ts t -> Int -> Int
 checkLookup lu scope =
   case lu of
-    Previous lu'  -> checkLookup lu' (scope - 1)
-    Prior n lu'   -> checkLookup lu' (scope - n)
-    _             -> scope
+    Prev lu'    -> checkLookup lu' (scope - 1)
+    PrevN n lu' -> checkLookup lu' (scope - n)
+    _           -> scope
 
 -- Returns the amount of signal elements needed to evaluate the predicate.
 minSigLengthForPred :: Pred ts -> Int -> Int
 minSigLengthForPred predicate acc =
     case predicate of
-      Not p           -> minSigLengthForPred p acc
-      And p1 p2       -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
-      Or p1 p2        -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
-      Until p1 p2     -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
-      Next p          -> minSigLengthForPred p (acc + 1)
-      Implies p1 p2   -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
-      Release p1 p2   -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
-      Always p        -> minSigLengthForPred p acc
-      Eventually p    -> minSigLengthForPred p acc
-      After n p       -> minSigLengthForPred p (acc + n)
-      _               -> acc
+      Not p     -> minSigLengthForPred p acc
+      And p1 p2 -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
+      Or p1 p2  -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
+      U p1 p2   -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
+      X p       -> minSigLengthForPred p (acc + 1)
+      p1 :=> p2 -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
+      R p1 p2   -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
+      G p       -> minSigLengthForPred p acc
+      F p       -> minSigLengthForPred p acc
+      XN n p    -> minSigLengthForPred p (acc + n)
+      _         -> acc
 
-nthPrevious :: Int -> Value t -> Maybe' (Value t)
-nthPrevious n curr@(Current b history)
+nthPrev :: Int -> Value t -> Maybe' (Value t)
+nthPrev n curr@(Current b history)
   | n <= 0    = Just' curr
   | otherwise =
       case history of
-        _ :! xs -> nthPrevious (n - 1) (Current b xs)
+        _ :! xs -> nthPrev (n - 1) (Current b xs)
         Nil     -> Nothing'
 
-evalTicked :: Lookup ts t -> HList ts -> Bool
-evalTicked lu hls = case lu of
-  Previous _ -> errorTickedPast
-  Prior _ _  -> errorTickedPast
-  First      -> extract $ first hls
-  Second     -> extract $ second hls
-  Third      -> extract $ third hls
-  Fourth     -> extract $ fourth hls
-  Fifth      -> extract $ fifth hls
-  Sixth      -> extract $ sixth hls
-  Seventh    -> extract $ seventh hls
-  Eighth     -> extract $ eighth hls
-  Ninth      -> extract $ ninth hls
+evalTick :: Lookup ts t -> HList ts -> Bool
+evalTick lu hls = case lu of
+  Prev _    -> errorTickPast
+  PrevN _ _ -> errorTickPast
+  Sig1      -> extract $ first hls
+  Sig2      -> extract $ second hls
+  Sig3      -> extract $ third hls
+  Sig4      -> extract $ fourth hls
+  Sig5      -> extract $ fifth hls
+  Sig6      -> extract $ sixth hls
+  Sig7      -> extract $ seventh hls
+  Sig8      -> extract $ eighth hls
+  Sig9      -> extract $ ninth hls
   where
-    errorTickedPast                   = error "Cannot check if signal has ticked in the past."
-    extract (Current (HasTicked b) _) = b
+    errorTickPast                   = error "Cannot check if signal has ticked in the past."
+    extract (Current (HasTick b) _) = b
 
 evalExpr :: Expr ts t -> HList ts -> Expr ts t
 evalExpr (Pure x) _      = pure x
-evalExpr (Apply f x) hls = (($) <$> evalExpr f hls) <*> evalExpr x hls
-evalExpr (Index lu) hls  =
+evalExpr (App f x) hls = (($) <$> evalExpr f hls) <*> evalExpr x hls
+evalExpr (Val lu) hls  =
   case evalLookup lu hls of
     Just' (Current _ (h :! _)) -> pure h
     Just' (Current _ Nil)      -> error "History not found for signal."
     Nothing'                   -> error "Signal not found."
-evalExpr (Ticked lu) hls = pure (evalTicked lu hls)
+evalExpr (Tick lu) hls = pure (evalTick lu hls)
 
 evalLookup :: Lookup ts t -> HList ts -> Maybe' (Value t)
 evalLookup lu hls = case lu of
-  Previous lu' ->
+  Prev lu' ->
     case evalLookup lu' hls of
       Just' (Current b history) ->
         case history of
           _ :! xs -> Just' (Current b xs)
           Nil     -> Nothing'
       Nothing' -> Nothing'
-  Prior n lu'  -> case evalLookup lu' hls of
-    Just' v  -> nthPrevious n v
+  PrevN n lu'  -> case evalLookup lu' hls of
+    Just' v  -> nthPrev n v
     Nothing' -> Nothing'
-  First         -> Just' (first hls)
-  Second        -> Just' (second hls)
-  Third         -> Just' (third hls)
-  Fourth        -> Just' (fourth hls)
-  Fifth         -> Just' (fifth hls)
-  Sixth         -> Just' (sixth hls)
-  Seventh       -> Just' (seventh hls)
-  Eighth        -> Just' (eighth hls)
-  Ninth         -> Just' (ninth hls)
+  Sig1 -> Just' (first hls)
+  Sig2 -> Just' (second hls)
+  Sig3 -> Just' (third hls)
+  Sig4 -> Just' (fourth hls)
+  Sig5 -> Just' (fifth hls)
+  Sig6 -> Just' (sixth hls)
+  Sig7 -> Just' (seventh hls)
+  Sig8 -> Just' (eighth hls)
+  Sig9 -> Just' (ninth hls)
 
 -- Evaluate a single timestep. Used exclusively for shrink cases.
 evaluateSingle  :: Int -> Pred ts -> Sig (HList ts) -> Bool
 evaluateSingle timestepsLeft formulae sig@(x ::: _) =
   timestepsLeft <= 0 || case formulae of
-            Tautology       -> True
-            Contradiction   -> False
+            TT -> True
+            FF -> False
             Now expr        ->
               case evalExpr expr x of
                 Pure b -> b
                 _ -> error "Unexpected error during evaluation."
-            Not phi         -> not (eval phi sig)
-            And phi psi     -> eval phi sig && eval psi sig
-            Or phi psi      -> eval phi sig || eval psi sig
-            Until phi psi   -> eval psi sig || eval phi sig
-            Next _          -> True
-            Implies phi psi -> not (eval phi sig && not (eval psi sig))
-            Always phi      -> eval phi sig
-            Eventually phi  -> eval phi sig 
-            Release _ _     -> True 
-            After _ _       -> True
+            Not phi     -> not (eval phi sig)
+            And phi psi -> eval phi sig && eval psi sig
+            Or phi psi  -> eval phi sig || eval psi sig
+            U phi psi   -> eval psi sig || eval phi sig
+            X _         -> True
+            phi :=> psi -> not (eval phi sig && not (eval psi sig))
+            G phi       -> eval phi sig
+            F phi       -> eval phi sig 
+            R _ _       -> True 
+            XN _ _      -> True
         where
           eval = evaluateSingle timestepsLeft
 
@@ -251,27 +290,27 @@
   if IntSet.null cl
     then evaluateSingle timestepsLeft formulae sig
     else timestepsLeft <= 0 || case formulae of
-            Tautology       -> True
-            Contradiction   -> False
-            Now expr        ->
+            TT   -> True
+            FF   -> False
+            Now expr ->
               case evalExpr expr x of
                 Pure b -> b
                 _ -> error "Unexpected error during evaluation."
-            Not phi         -> not (eval phi sig)
-            And phi psi     -> eval phi sig && eval psi sig
-            Or phi psi      -> eval phi sig || eval psi sig
-            Until phi psi   -> eval psi sig
-                              || (eval phi sig && evaluateNext (phi `Until` psi) advance)
-            Next phi        -> evaluateNext phi advance
-            Implies phi psi -> not (eval phi sig && not (eval psi sig))
-            Always phi      -> eval phi sig && evaluateNext (Always phi) advance
-            Eventually phi  -> (eval phi sig || evaluateNext (Eventually phi) advance)
+            Not phi     -> not (eval phi sig)
+            And phi psi -> eval phi sig && eval psi sig
+            Or phi psi  -> eval phi sig || eval psi sig
+            U phi psi   -> eval psi sig
+                              || (eval phi sig && evaluateX (phi `U` psi) advance)
+            X phi       -> evaluateX phi advance
+            phi :=> psi -> not (eval phi sig && not (eval psi sig))
+            G phi       -> eval phi sig && evaluateX (G phi) advance
+            F phi       -> (eval phi sig || evaluateX (F phi) advance)
                                 && not (timestepsLeft == 1 && not (eval phi sig))
-            Release phi psi -> (eval psi sig && eval phi sig)
-                                || (eval psi sig && evaluateNext (phi `Until` psi) advance)
-            After n phi     -> if n <= 0 then eval phi sig else evaluateNext (After (n - 1) phi) sig
+            R phi psi   -> (eval psi sig && eval phi sig)
+                                || (eval psi sig && evaluateX (phi `U` psi) advance)
+            XN n phi    -> if n <= 0 then eval phi sig else evaluateX (XN (n - 1) phi) sig
       where
-        evaluateNext = evaluate' (timestepsLeft - 1)
+        evaluateX = evaluate' (timestepsLeft - 1)
         eval = evaluate' timestepsLeft
         advance = f (InputValue (IntSet.findMin cl) ())
 
@@ -288,7 +327,7 @@
       scopeOk   = checkScope p
   in 
     if not scopeOk
-      then error "Previous must be in scope of next" 
+      then error "Prev must be in scope of X" 
     else if min' > defaultTimeStepsToCheck
       then error ("Cannot evaluate more than " ++ show defaultTimeStepsToCheck ++ " values.\n" ++ "Predicate requires " ++ show min' ++ " timesteps. Consider using evaluateWith (>= " ++ show min' ++ ")")
     else
diff --git a/src/PropRatt/Value.hs b/src/PropRatt/Value.hs
--- a/src/PropRatt/Value.hs
+++ b/src/PropRatt/Value.hs
@@ -6,16 +6,20 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ScopedTypeVariables, UndecidableInstances #-}
 
-module PropRatt.Value (Value(..),pureVal,current, HasTicked(..)) where
+module PropRatt.Value (Value(..),pureVal,current, HasTick(..)) where
 import AsyncRattus.Strict
 import AsyncRattus.Signal hiding (current)
 import PropRatt.Utils
 import AsyncRattus
 
-newtype HasTicked = HasTicked Bool deriving Show
+newtype HasTick = HasTick Bool
 
+instance Show HasTick where
+  show (HasTick True) = "!"
+  show (HasTick False) = "_"
+
 data Value a where
-  Current :: !HasTicked -> !(List a) -> Value a
+  Current :: !HasTick -> !(List a) -> Value a
 
 instance Stable (Value a) where 
 instance Num a => Num (Value a) where
@@ -29,8 +33,7 @@
 
 instance Show a => Show (Value a) where
   show (Current t Nil) = show t
-  show (Current _ (h :! Nil)) = show h
-  show (Current _ (h :! h2 :! _)) =  show h ++ " " ++ show h2
+  show (Current t (h :! _)) = show t ++ show h
 
 instance Show a => Show (Sig [Value a]) where
   show sig = "Sig [Value a]: " ++ show (toListOfLength 100 sig) ++ "..."
@@ -42,7 +45,7 @@
   v1 == v2 = current v1 == current v2
 
 pureVal :: a -> Value a
-pureVal x = Current (HasTicked False) (x :! Nil)
+pureVal x = Current (HasTick False) (x :! Nil)
 
 current :: Value a -> a
 current (Current _ (h :! _)) = h