PiCalcOpenBisim.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    ":opt no-lint -- turn off lint messages"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## module PiCalc"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "{-# LANGUAGE FlexibleContexts          #-}\n",
    "{-# LANGUAGE FlexibleInstances         #-}\n",
    "{-# LANGUAGE MultiParamTypeClasses     #-}\n",
    "{-# LANGUAGE NoMonomorphismRestriction #-}\n",
    "{-# LANGUAGE ScopedTypeVariables       #-}\n",
    "{-# LANGUAGE DeriveGeneric             #-}\n",
    "{-# LANGUAGE UndecidableInstances      #-}\n",
    "\n",
    "module PiCalc where\n",
    "import GHC.Generics (Generic)\n",
    "import Data.Maybe\n",
    "import Data.List\n",
    "import Unbound.Generics.LocallyNameless\n",
    "\n",
    "type Nm = Name Tm\n",
    "newtype Tm = Var Nm deriving (Eq, Ord, Show, Generic)\n",
    "\n",
    "data Pr  = Null | TauP Pr | Out Tm Tm Pr | In Tm PrB | Match Tm Tm Pr\n",
    "         | Plus Pr Pr | Par Pr Pr | Nu PrB  deriving (Eq, Ord, Show, Generic)\n",
    "type PrB = Bind Nm Pr\n",
    "instance Eq PrB where (==) = aeq\n",
    "instance Ord PrB where compare = acompare\n",
    "\n",
    "data Act   = Up Tm Tm  | Tau     deriving (Eq, Ord, Show, Generic)\n",
    "data ActB  = UpB Tm    | DnB Tm  deriving (Eq, Ord, Show, Generic)\n",
    "\n",
    "data Form  = FF | TT | Conj [Form] | Disj [Form]\n",
    "           | Dia  Act Form  |  DiaB  ActB FormB   | DiaMatch [(Tm,Tm)]\n",
    "           | Box  Act Form  |  BoxB  ActB FormB   | BoxMatch [(Tm,Tm)] Form\n",
    "           deriving (Eq, Ord, Show, Generic)\n",
    "type FormB = Bind Nm Form\n",
    "instance Eq FormB where (==) = aeq\n",
    "instance Ord FormB where compare = acompare\n",
    "\n",
    "instance Alpha Tm; instance Alpha Act; instance Alpha ActB\n",
    "instance Alpha Pr; instance Alpha Form\n",
    "\n",
    "instance Subst Tm Tm where isvar (Var x) = Just (SubstName x)\n",
    "instance Subst Tm Act;  instance Subst Tm ActB\n",
    "instance Subst Tm Pr;  instance Subst Tm Form\n",
    "\n",
    "infixr 1 .\\\n",
    "(.\\) = bind\n",
    "\n",
    "x .= y = Match (Var x) (Var y)\n",
    "inp = In . Var\n",
    "out x y = Out(Var x)(Var y)\n",
    "tau = TauP Null\n",
    "tautau = TauP (TauP Null)\n",
    "\n",
    "conj  = cn . filter(/=TT) where cn  [] = TT; cn  [f] = f; cn  fs = Conj fs\n",
    "disj  = ds . filter(/=FF) where ds  [] = FF; ds  [f] = f; ds  fs = Disj fs\n",
    "\n",
    "unbind2' b1 b2 = do  Just (x,p1,_,p2) <- unbind2 b1 b2\n",
    "                     return (x,p1,p2)\n",
    "(.+)  = Plus  ;   infixl 6 .+\n",
    "(.|)  = Par   ;  infixl 5 .|\n",
    "o = Null\n",
    "taup = TauP\n",
    "nu = Nu\n",
    "\n",
    "\n",
    "{- To port these, may need DeriveDataTypeable\n",
    "------------------------------------------------------------------\n",
    "-- transformation/reduction of processes via generic programming\n",
    "------------------------------------------------------------------\n",
    "removeNull :: Rep a => a -> a\n",
    "removeNull a = case cast a of\n",
    "  Just(Plus Null x) -> fromJust(cast x)\n",
    "  Just(Plus x Null) -> fromJust(cast x)\n",
    "  Just(Par Null x) -> fromJust(cast x)\n",
    "  Just(Par x Null) -> fromJust(cast x)\n",
    "  _ -> a\n",
    "-- rotate right for associative operators Plus and Par\n",
    "rotateRight :: Rep a => a -> a\n",
    "rotateRight a = case cast a of\n",
    "  Just(Plus (Plus x y) z) -> fromJust . cast $ Plus x (Plus y z)\n",
    "  Just(Par (Par x y) z) -> fromJust . cast $ Par x (Par y z)\n",
    "  _ -> a\n",
    "-- nub/sort for commutative operators Plus and Par\n",
    "nubSortComm :: Rep a => a -> a\n",
    "nubSortComm a = case cast a of\n",
    "  Just p@(Plus _ _) -> fromJust . cast . foldr1 Plus . nubSort $\n",
    "    unfoldr (\\q -> case q of { Plus x y -> Just(x,y) ; _ -> Nothing }) p\n",
    "  Just p@(Par _ _) -> fromJust . cast . foldr1 Par . nubSort $\n",
    "    unfoldr (\\q -> case q of { Par x y -> Just(x,y) ; _ -> Nothing }) p\n",
    "  _ -> a\n",
    "simplify = everywhere nubSortComm\n",
    "         . everywhere rotateRight\n",
    "         . everywhere removeNull\n",
    "{-\n",
    "foldl1 Plus (replicate 3 $ foldl1 Par [Null,Null,Null])\n",
    "everywhere rotateRight $ foldl1 Plus (replicate 3 $ foldl1 Par [Null,Null,Null])\n",
    "red $ foldl1 Plus (replicate 3 $ foldl1 Par [Null,Null,Null])\n",
    "-}\n",
    "-}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## module MemoUgly"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "{-# LANGUAGE NoMonomorphismRestriction #-}\n",
    "module MemoUgly where\n",
    "import Control.Concurrent.MVar\n",
    "import qualified Data.Map as M\n",
    "import System.IO.Unsafe(unsafePerformIO)\n",
    "import qualified Data.MemoUgly\n",
    "\n",
    "memo = Data.MemoUgly.memo\n",
    "memoIO = Data.MemoUgly.memoIO\n",
    "\n",
    "memoFix ff = f where f = memo (ff f)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "{-# LANGUAGE FlexibleContexts          #-}\n",
    "{-# LANGUAGE FlexibleInstances         #-}\n",
    "{-# LANGUAGE MultiParamTypeClasses     #-}\n",
    "{-# LANGUAGE NoMonomorphismRestriction #-}\n",
    "{-# LANGUAGE ScopedTypeVariables       #-}\n",
    "{-# LANGUAGE UndecidableInstances      #-}\n",
    "\n",
    "module IdSubLTS where\n",
    "import           Control.Applicative\n",
    "import           Control.Monad\n",
    "import           Control.Monad.Fail\n",
    "import           PiCalc\n",
    "import           Unbound.Generics.LocallyNameless\n",
    "\n",
    "-- one :: (Fresh m, Alternative m, MonadFail m) => Pr -> m (Act, Pr)\n",
    "one (Out x y p)    = return (Up x y, p)\n",
    "one (TauP p)       = return (Tau, p)\n",
    "one (Match x y p)  | x == y = one p\n",
    "one (Plus p q) = one p <|> one q\n",
    "one (Par p q)\n",
    "  =    do  (l, p') <- one p;  return (l, Par p' q)\n",
    "  <|>  do  (l, q') <- one q;  return (l, Par p q')\n",
    "  <|>  do  (lp, bp) <- oneb p;  (lq, bq) <- oneb q\n",
    "           case (lp, lq) of  (UpB x,DnB x') | x == x'           -- close\n",
    "                                            -> do  (y, p', q') <- unbind2' bp bq\n",
    "                                                   return (Tau, Nu(y.\\Par p' q'))\n",
    "                             (DnB x',UpB x) | x' == x           -- close\n",
    "                                            -> do  (y, q', p') <- unbind2' bq bp\n",
    "                                                   return (Tau, Nu(y.\\Par p' q'))\n",
    "                             _              -> empty\n",
    "  <|>  do  (Up x v, p') <- one p;  (DnB x', (y,q')) <- oneb' q\n",
    "           guard $ x == x'\n",
    "           return (Tau, Par p' (subst y v q'))  -- interaction\n",
    "  <|>  do  (DnB x', (y,p')) <- oneb' p;  (Up x v, q') <- one q\n",
    "           guard $ x == x'\n",
    "           return (Tau, Par (subst y v p') q')  -- interaction\n",
    "one (Nu b)  = do  (x,p) <- unbind b\n",
    "                  (l,p') <- one p\n",
    "                  case l of  Up (Var x') (Var y)  | x == x'  -> empty\n",
    "                                                  | x == y   -> empty\n",
    "                             _                    -> return (l, Nu (x.\\p'))\n",
    "one _       = empty\n",
    "\n",
    "-- oneb :: (Fresh m, Alternative m, MonadFail m) => Pr -> m (ActB, PrB)\n",
    "oneb (In x p)      = return (DnB x, p)\n",
    "oneb (Match x y p) | x == y = oneb p\n",
    "oneb (Plus p q)  = oneb p <|> oneb q\n",
    "oneb (Par p q)   =     do  (l,(x,p')) <- oneb' p;  return (l, x.\\Par p' q)\n",
    "                 <|>   do  (l,(x,q')) <- oneb' q;  return (l, x.\\Par p q')\n",
    "oneb (Nu b)      =     do  (x,p) <- unbind b\n",
    "                           (l,(y,p')) <- oneb' p\n",
    "                           case l of  UpB (Var x')   | x == x' -> empty\n",
    "                                      DnB (Var x')   | x == x' -> empty\n",
    "                                      _              -> return (l, y.\\Nu (x.\\p'))\n",
    "                 <|>   do  (x,p) <- unbind b\n",
    "                           (Up y (Var x'),p') <- one p\n",
    "                           guard $ x == x' && Var x /= y\n",
    "                           return (UpB y, x.\\p')  -- open\n",
    "oneb _           = empty\n",
    "\n",
    "oneb' p = do (l,b) <- oneb p; r <- unbind b; return (l,r)\n",
    "\n",
    "{-\n",
    "% Finite pi-calculus specification in lambda-Prolog\n",
    "% A specification of the late transition system for the finite pi calculus.\n",
    "% bound input\n",
    "oneb (in X M) (dn X) M.\n",
    "% free output\n",
    "one (out X Y P) (up X Y) P.\n",
    "% tau\n",
    "one  (taup P) tau P.\n",
    "% match prefix\n",
    "one  (match X X P) A Q :- one  P A Q.\n",
    "oneb (match X X P) A M :- oneb P A M.\n",
    "% sum\n",
    "one  (plus P Q) A R :- one  P A R.\n",
    "one  (plus P Q) A R :- one  Q A R.\n",
    "oneb (plus P Q) A M :- oneb P A M.\n",
    "oneb (plus P Q) A M :- oneb Q A M.\n",
    "% par\n",
    "one  (par P Q) A (par P1 Q) :- one P A P1.\n",
    "one  (par P Q) A (par P Q1) :- one Q A Q1.\n",
    "oneb (par P Q) A (x\\par (M x) Q) :- oneb P A M.\n",
    "oneb (par P Q) A (x\\par P (N x)) :- oneb Q A N.\n",
    "% restriction\n",
    "one  (nu x\\P x) A (nu x\\Q x)      :- pi x\\ one  (P x) A (Q x).\n",
    "oneb (nu x\\P x) A (y\\ nu x\\Q x y) :- pi x\\ oneb (P x) A (y\\ Q x y).\n",
    "% open\n",
    "oneb (nu x\\M x) (up X) N :- pi y\\ one (M y) (up X y) (N y).\n",
    "% close\n",
    "one (par P Q) tau (nu y\\ par (M y) (N y)) :- oneb P (dn X) M , oneb Q (up X) N.\n",
    "one (par P Q) tau (nu y\\ par (M y) (N y)) :- oneb P (up X) M , oneb Q (dn X) N.\n",
    "% comm\n",
    "one (par P Q) tau (par (M Y) T) :-  oneb P (dn X) M, one Q (up X Y) T.\n",
    "one (par P Q) tau (par R (M Y)) :-  oneb Q (dn X) M, one P (up X Y) R.\n",
    "-}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## module OpenLTS"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "{-# LANGUAGE FlexibleContexts          #-}\n",
    "{-# LANGUAGE FlexibleInstances         #-}\n",
    "{-# LANGUAGE MultiParamTypeClasses     #-}\n",
    "{-# LANGUAGE NoMonomorphismRestriction #-}\n",
    "{-# LANGUAGE ScopedTypeVariables       #-}\n",
    "{-# LANGUAGE UndecidableInstances      #-}\n",
    "{-# LANGUAGE DeriveGeneric             #-}\n",
    "module OpenLTS where\n",
    "import           GHC.Generics (Generic)\n",
    "import           Control.Applicative\n",
    "import           Control.Lens.Fold\n",
    "import           Control.Monad\n",
    "import           Control.Monad.Fail\n",
    "import           Data.Map.Strict         (Map (..), fromList, insert, (!))\n",
    "import           Data.Partition          hiding (empty, rep)\n",
    "import qualified Data.Partition          as P\n",
    "import           PiCalc\n",
    "import           Unbound.Generics.LocallyNameless hiding (fv)\n",
    "import qualified Unbound.Generics.LocallyNameless as U\n",
    "{-# ANN module \"HLint: ignore Use mappend\" #-}\n",
    "{-# ANN module \"HLint: ignore Use camelCase\" #-}\n",
    "\n",
    "fv = toListOf U.fv\n",
    "\n",
    "type EqC = [(Nm,Nm)]\n",
    "{-\n",
    "infixr 5 .:\n",
    "(.:) :: (Nm,Nm) -> EqC -> EqC\n",
    "(x,y) .: sigma = case compare x y of  LT -> [(x,y)] .++ sigma\n",
    "                                      EQ -> sigma\n",
    "                                      GT -> [(y,x)] .++ sigma\n",
    "infixr 5 .++\n",
    "(.++) = union\n",
    "-}\n",
    "\n",
    "type Ctx = [Quan]\n",
    "data Quan = All Nm | Nab Nm deriving (Eq, Ord, Show, Generic)\n",
    "quan2nm :: Quan -> Nm\n",
    "quan2nm (All x) = x\n",
    "quan2nm (Nab x) = x\n",
    "\n",
    "instance Alpha Quan\n",
    "instance Subst Tm Quan\n",
    "\n",
    "\n",
    "-- wrapper -------------------\n",
    "one nctx p = do (sigma, r) <- one_ ctx p\n",
    "                return (part2eqc ctx sigma, r)\n",
    "  where ctx = toCtx' nctx\n",
    "oneb nctx b = do (sigma, r) <- one_b ctx b\n",
    "                 return (part2eqc ctx sigma, r)\n",
    "  where ctx = toCtx' nctx\n",
    "-----------------------------\n",
    "\n",
    "type Ctx' = (Ctx, Int, Map Nm Int)\n",
    "emptyCtx' = ([], 0, fromList [])\n",
    "type EqC' = Partition Int\n",
    "\n",
    "toCtx' :: Ctx -> Ctx'\n",
    "toCtx' nctx = (nctx, maxVal, n2iMap)\n",
    "  where\n",
    "    revns = reverse (fv nctx)\n",
    "    n2iMap = fromList $ zip revns [0..maxVal]\n",
    "    maxVal = length nctx - 1\n",
    "\n",
    "extend :: Quan -> Ctx' -> Ctx'\n",
    "extend q (nctx, n, n2iMap) = (q:nctx, n+1, insert (quan2nm q) (n+1) n2iMap)\n",
    "\n",
    "respects :: EqC -> Ctx -> Bool\n",
    "respects sigma nctx = all (\\n -> P.rep part n == n) [n2i x | Nab x <- nctx]\n",
    "  where (part, (n2i, _)) = mkPartitionFromEqC nctx sigma\n",
    "\n",
    "respects' :: EqC -> Ctx' -> Bool\n",
    "respects' sigma ctx@(nctx,_,n2iMap) =\n",
    "  all (\\n -> P.rep part n == n) [n2i x | Nab x <- nctx]\n",
    "  where (part,(n2i,i2n)) = mkPartitionFromEqC' ctx sigma\n",
    "\n",
    "respects_ :: EqC' -> Ctx' -> Bool\n",
    "respects_ sigma ctx@(nctx,_,n2iMap) =\n",
    "  all (\\n -> P.rep sigma n == n) [n2i x | Nab x <- nctx]\n",
    "  where (n2i,i2n) = mkMapFunsFromEqC' ctx sigma\n",
    "\n",
    "subs :: Subst Tm b => Ctx -> EqC -> b -> b\n",
    "subs nctx sigma = substs [(x,Var y) | (x,y)<-sigma']\n",
    "  where  sigma' = [(i2n i, i2n $ P.rep part i) | i<-[0..maxVal]]\n",
    "         (part, (n2i, i2n)) = mkPartitionFromEqC nctx sigma\n",
    "         maxVal = length nctx - 1\n",
    "\n",
    "subs_ :: Subst Tm b => Ctx' -> EqC' -> b -> b\n",
    "subs_ ctx@(nctx,maxVal,n2iMap) sigma = substs [(x,Var y) | (x,y)<-sigma']\n",
    "  where  sigma' = [(i2n i, i2n $ P.rep sigma i) | i<-[0..maxVal]]\n",
    "         (n2i, i2n) = mkMapFunsFromEqC' ctx sigma\n",
    "\n",
    "mkPartitionFromEqC ::  Ctx -> EqC -> (Partition Int, (Nm -> Int, Int -> Nm))\n",
    "mkPartitionFromEqC nctx sigma = (part, (n2i, i2n))\n",
    "  where\n",
    "    part =  foldr (.) id [joinElems (n2i x) (n2i y) | (x,y) <- sigma] discrete\n",
    "    i2n i = revns !! i\n",
    "    n2i x = n2iMap ! x\n",
    "    revns = reverse (fv nctx)\n",
    "    n2iMap = fromList $ zip revns [0..maxVal]\n",
    "    maxVal = length nctx - 1\n",
    "\n",
    "mkPartitionFromEqC' :: Ctx' -> EqC -> (Partition Int, (Nm -> Int, Int -> Nm))\n",
    "mkPartitionFromEqC' (nctx,maxVal,n2iMap) sigma = (part, (n2i, i2n))\n",
    "  where\n",
    "    part =  foldr (.) id [joinElems (n2i x) (n2i y) | (x,y) <- sigma] discrete\n",
    "    i2n i = quan2nm $ nctx !! (maxVal - i)\n",
    "    n2i x = n2iMap ! x\n",
    "\n",
    "joinNm ctx (x,y) sigma = joinElems (n2i x) (n2i y) sigma\n",
    "  where (n2i,i2n) = mkMapFunsFromEqC' ctx sigma\n",
    "\n",
    "joinParts sigma_p sigma_q = fromSets $ nontrivialSets sigma_p ++ nontrivialSets sigma_q\n",
    "\n",
    "mkMapFunsFromEqC' :: Ctx' -> EqC' -> (Nm -> Int, Int -> Nm)\n",
    "mkMapFunsFromEqC' (nctx,maxVal,n2iMap) sigma = (n2i, i2n)\n",
    "  where\n",
    "    i2n i = quan2nm $ nctx !! (maxVal - i)\n",
    "    n2i x = n2iMap ! x\n",
    "\n",
    "part2eqc :: Ctx' -> EqC' -> EqC\n",
    "part2eqc ctx@(nctx,maxVal,n2iMap) sigma =\n",
    "  [(i2n i, i2n j) | (i,j) <- [(i, P.rep sigma i) | i<-[0..maxVal]], i/=j]\n",
    "  where (n2i,i2n) = mkMapFunsFromEqC' ctx sigma\n",
    "\n",
    "-- one_ :: (Fresh m, Alternative m) => Ctx' -> Pr -> m (EqC',(Act,Pr))\n",
    "one_ ctx  (Out x y p)   = return (P.empty, (Up x y, p))\n",
    "one_ ctx  (TauP p)      = return (P.empty, (Tau, p))\n",
    "one_ ctx  (Match (Var x) (Var y) p)  | x == y                   = one_ ctx p\n",
    "                                     | [(x,y)] `respects'` ctx  =\n",
    "                                           do  (sigma, r) <- one_ ctx p\n",
    "                                               let sigma' = joinNm ctx (x,y) sigma\n",
    "                                               guard $ sigma' `respects_` ctx\n",
    "                                               return (sigma', r)\n",
    "one_ ctx  (Plus p q) = one_ ctx p <|> one_ ctx q\n",
    "one_ ctx  (Par p q)\n",
    "  =    do  (sigma,(l,p')) <- one_ ctx p;  return (sigma,(l,Par p' q))\n",
    "  <|>  do  (sigma,(l,q')) <- one_ ctx q;  return (sigma,(l,Par p q'))\n",
    "  <|>  do  (sigma_p,(lp,bp)) <- one_b ctx p;  (sigma_q,(lq,bq)) <- one_b ctx q\n",
    "           case (lp, lq) of             -- close\n",
    "             (DnB(Var x),UpB(Var x'))  -> do  (y, q', p') <-  unbind2' bq bp\n",
    "                                              let sigma' = joinNm ctx (x,x') (joinParts sigma_p sigma_q)\n",
    "                                              guard $ sigma' `respects_` ctx\n",
    "                                              return (sigma', (Tau, Nu(y.\\Par p' q')))\n",
    "             (UpB(Var x'),DnB(Var x))  -> do  (y, p', q') <- unbind2' bp bq\n",
    "                                              let sigma' = joinNm ctx (x,x') (joinParts sigma_p sigma_q)\n",
    "                                              guard $ sigma' `respects_` ctx\n",
    "                                              return (sigma', (Tau, Nu(y.\\Par p' q')))\n",
    "             _                         -> empty\n",
    "  <|>  do  (sigma_p, (Up (Var x) v, p')) <- one_ ctx p\n",
    "           (sigma_q, (DnB (Var x'), bq)) <- one_b ctx q;  (y, q') <- unbind bq\n",
    "           let sigma' = joinNm ctx (x,x') (joinParts sigma_p sigma_q)\n",
    "           guard $ sigma' `respects_` ctx\n",
    "           return (sigma', (Tau, Par p' (subst y v q'))) -- interaction\n",
    "  <|>  do  (sigma_p, (DnB (Var x'), (y, p')))   <- one_b'  ctx p\n",
    "           (sigma_q, (Up (Var x) v,     q'))    <- one_    ctx q\n",
    "           let sigma' = joinNm ctx (x,x') (joinParts sigma_p sigma_q)\n",
    "           guard $ sigma' `respects_` ctx\n",
    "           return (sigma', (Tau, Par (subst y v p') q'))\n",
    "one_ ctx (Nu b) = do  (x,p) <- unbind b;              let ctx' = extend (Nab x) ctx\n",
    "                      (sigma,(l,p')) <- one_ ctx' p;  let sigmaSubs = subs_ ctx' sigma\n",
    "                      case l of  Up (Var x') (Var y)  | x == sigmaSubs x'  -> empty\n",
    "                                                      | x == sigmaSubs y   -> empty\n",
    "                                 _                    -> return (sigma, (l, Nu(x.\\p')))\n",
    "one_ _    _      = empty\n",
    "\n",
    "-- one_b :: (Fresh m, Alternative m) => Ctx' -> Pr -> m (EqC',(ActB, PrB))\n",
    "one_b ctx (In x p) = return (P.empty, (DnB x, p))\n",
    "one_b ctx (Match (Var x) (Var y) p)  | x == y                   = one_b ctx p\n",
    "                                     | [(x,y)] `respects'` ctx  =\n",
    "                                           do  (sigma, r) <- one_b ctx p\n",
    "                                               let sigma' = joinNm ctx (x,y) sigma\n",
    "                                               guard $ sigma' `respects_` ctx\n",
    "                                               return (sigma', r)\n",
    "one_b ctx (Plus p q) = one_b ctx p <|> one_b ctx q\n",
    "one_b ctx (Par p q) =\n",
    "       do (sigma,(l,(x,p'))) <- one_b' ctx p;  return (sigma,(l, x.\\Par p' q))\n",
    "  <|>  do (sigma,(l,(x,q'))) <- one_b' ctx q;  return (sigma,(l, x.\\Par p q'))\n",
    "one_b ctx (Nu b)  =    do  (x,p) <- unbind b;                    let ctx' = extend (Nab x) ctx\n",
    "                           (sigma,(l,(y,p'))) <- one_b' ctx' p;  let sigmaSubs = subs_ ctx' sigma\n",
    "                           case l of  UpB (Var x')  | x == sigmaSubs x' -> empty\n",
    "                                      DnB (Var x')  | x == sigmaSubs x' -> empty\n",
    "                                      _             -> return (sigma, (l, y.\\Nu (x.\\p')))\n",
    "                  <|>  do  (x,p) <- unbind b;                          let ctx' = extend (Nab x) ctx\n",
    "                           (sigma,(Up y (Var x'),p')) <- one_ ctx' p;  let sigmaSubs = subs_ ctx' sigma\n",
    "                           guard $ x == sigmaSubs x' && Var x /= sigmaSubs y\n",
    "                           return (sigma, (UpB y, x.\\p')) -- open\n",
    "one_b _    _ = empty\n",
    "\n",
    "one_b' ctx p = do (sigma,(l,b)) <- one_b ctx p; r <- unbind b; return (sigma,(l,r))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## module OpenBisim"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "{-# LANGUAGE FlexibleContexts          #-}\n",
    "{-# LANGUAGE FlexibleInstances         #-}\n",
    "{-# LANGUAGE MultiParamTypeClasses     #-}\n",
    "{-# LANGUAGE NoMonomorphismRestriction #-}\n",
    "{-# LANGUAGE ScopedTypeVariables       #-}\n",
    "{-# LANGUAGE UndecidableInstances      #-}\n",
    "module OpenBisim where\n",
    "import           Control.Applicative\n",
    "import           Control.Lens.Fold\n",
    "import           Control.Monad\n",
    "import           Control.Monad.Fail\n",
    "import qualified Control.Monad.Fail as Fail\n",
    "import           Data.Tree\n",
    "import qualified IdSubLTS as IdS\n",
    "import           MemoUgly\n",
    "import           OpenLTS                 hiding (one, oneb)\n",
    "import           PiCalc\n",
    "import           Unbound.Generics.LocallyNameless hiding (fv)\n",
    "{-# ANN module \"HLint: ignore Use mappend\" #-}\n",
    " \n",
    "instance MonadFail f => MonadFail (FreshMT f) where\n",
    "  fail = runFreshMT . Fail.fail\n",
    "\n",
    "data StepLog  =  One   Ctx EqC Act   Pr\n",
    "              |  OneB  Ctx EqC ActB  PrB  deriving (Eq,Ord,Show)\n",
    "\n",
    "returnL log = return . Node (Left log)   -- for the step on |p|'s side\n",
    "returnR log = return . Node (Right log)  -- for the step on |q|'s side\n",
    "\n",
    "-- wrapper -----------------------------\n",
    "sim nctx = sim2 (toCtx' nctx)\n",
    "sim' nctx = sim2' (toCtx' nctx)\n",
    "bisim nctx = bisim2 (toCtx' nctx)\n",
    "bisim' nctx = bisim2' (toCtx' nctx)\n",
    "----------------------------------------\n",
    "\n",
    "sim2 ctx p q = and $ sim2_ ctx p q\n",
    "\n",
    "sim2_ :: Ctx' -> Pr -> Pr -> [Bool]\n",
    "sim2_ ctx p q = memoFix sim2_unfix (ctx,p,q)\n",
    "\n",
    "sim2_unfix f (ctx@(nctx,_,_), p, q)  =\n",
    "       do  (sigma, r) <- runFreshMT (one_ ctx p); let sigmaSubs = subs_ ctx sigma\n",
    "           let (lp, p') = sigmaSubs r\n",
    "           return . (or :: [Bool] -> Bool) . runFreshMT $ do\n",
    "             (lq, q') <-IdS.one (sigmaSubs q)\n",
    "             guard $ lp == lq\n",
    "             return . (and :: [Bool] -> Bool) $ f(ctx,p',q')\n",
    "   <|>  do  (sigma, r) <- runFreshMT (one_b ctx p); let sigmaSubs = subs_ ctx sigma\n",
    "            let (lp, bp') = sigmaSubs r\n",
    "            let x' = runFreshM $ freshFrom (fv nctx) bp'\n",
    "            return . (or :: [Bool] -> Bool) . runFreshMT $ do\n",
    "              (lq, bq') <-IdS.oneb (sigmaSubs q)\n",
    "              guard $ lp == lq\n",
    "              (x, q1, p1) <- unbind2' bq' bp'\n",
    "              let (p', q')  | x == x'    = (p1, q1)\n",
    "                            | otherwise  = subst x (Var x') (p1, q1)\n",
    "              let ctx' = case lp of   DnB _ -> extend (All x') ctx\n",
    "                                      UpB _ -> extend (Nab x') ctx\n",
    "              return . (and :: [Bool] -> Bool) $ f(ctx',p',q')\n",
    "\n",
    "-- sim2' :: Ctx' -> Pr -> Pr -> [Tree (Either StepLog StepLog)]\n",
    "sim2' ctx@(nctx,_,_) p q   =\n",
    "        do   (sigma, r) <- runFreshMT (one_ ctx p); let sigmaSubs = subs_ ctx sigma\n",
    "             let (lp, p') = sigmaSubs r\n",
    "             returnL (One nctx (toEqC sigma) lp p') . runFreshMT $ do\n",
    "               (lq, q') <-IdS.one (sigmaSubs q)\n",
    "               guard $ lp == lq\n",
    "               returnR (One nctx (toEqC sigma) lq q') $ sim2' ctx p' q'\n",
    "  <|>   do   (sigma, r) <- runFreshMT (one_b ctx p); let sigmaSubs = subs_ ctx sigma\n",
    "             let (lp, bp') = sigmaSubs r\n",
    "             let x' = runFreshM $ freshFrom (fv nctx) bp'\n",
    "             returnL (OneB nctx (toEqC sigma) lp bp') . runFreshMT $ do\n",
    "               (lq, bq') <-IdS.oneb (sigmaSubs q)\n",
    "               guard $ lp == lq\n",
    "               (x, p1, q1) <- unbind2' bp' bq'\n",
    "               let (p', q')   | x == x'    = (p1, q1)\n",
    "                              | otherwise  = subst x (Var x') (p1, q1)\n",
    "               let ctx' = case lp of   DnB _ -> extend (All x') ctx\n",
    "                                       UpB _ -> extend (Nab x') ctx\n",
    "               returnR (OneB nctx (toEqC sigma) lq bq') $ sim2' ctx' p' q'\n",
    "  where toEqC = part2eqc ctx\n",
    "\n",
    "bisim2 ctx p q = and $ bisim2_ ctx p q -- (simplify p) (simplify q)\n",
    "\n",
    "bisim2_ ctx p q = memoFix bisim2_unfix (ctx,p,q)\n",
    "bisim2_unfix f (ctx@(nctx,_,_),p,q) =\n",
    "  do (sigma, r) <- runFreshMT (one_ ctx p)\n",
    "     let (lp, p') = subs_ ctx sigma r\n",
    "     return . (or :: [Bool] -> Bool) . runFreshMT $ do\n",
    "       (lq, q') <-IdS.one (subs_ ctx sigma q) -- follow with same sub and label\n",
    "       guard $ lp == lq\n",
    "       return . (and :: [Bool] -> Bool) $ f(ctx,p',q')\n",
    "  <|>\n",
    "  do (sigma, r) <- runFreshMT (one_b ctx p)\n",
    "     let (lp, bp') = subs_ ctx sigma r\n",
    "     let x' = runFreshM $ freshFrom (fv nctx) bp' -- to use same new quan var\n",
    "     return . (or :: [Bool] -> Bool) . runFreshMT $ do\n",
    "       (lq, bq') <-IdS.oneb (subs_ ctx sigma q) -- follow with same sub and label\n",
    "       guard $ lp == lq\n",
    "       (x, p1, q1) <- unbind2' bp' bq'\n",
    "       let (p', q') | x == x'   = (p1, q1) -- to use same new quan var\n",
    "                    | otherwise = subst x (Var x') (p1, q1)\n",
    "       let ctx' = case lp of DnB _ -> extend (All x') ctx\n",
    "                             UpB _ -> extend (Nab x') ctx\n",
    "       return . (and :: [Bool] -> Bool) $ f(ctx',p',q')\n",
    "  <|>\n",
    "  do (sigma, r) <- runFreshMT (one_ ctx q)\n",
    "     let (lq, q') = subs_ ctx sigma r\n",
    "     return . (or :: [Bool] -> Bool) . runFreshMT $ do\n",
    "       (lp, p') <-IdS.one (subs_ ctx sigma p) -- follow with same sub and label\n",
    "       guard $ lp == lq\n",
    "       return . (and :: [Bool] -> Bool) $ f(ctx,p',q')\n",
    "  <|>\n",
    "  do (sigma, r) <- runFreshMT (one_b ctx q)\n",
    "     let (lq, bq') = subs_ ctx sigma r\n",
    "     let x' = runFreshM $ freshFrom (fv nctx) bq' -- to use same new quan var\n",
    "     return . (or :: [Bool] -> Bool) . runFreshMT $ do\n",
    "       (lp, bp') <-IdS.oneb (subs_ ctx sigma p) -- follow with same sub and label\n",
    "       guard $ lp == lq\n",
    "       (x, q1, p1) <- unbind2' bq' bp'\n",
    "       let (p', q') | x == x'   = (p1, q1) -- to use same new quan var\n",
    "                    | otherwise = subst x (Var x') (p1, q1)\n",
    "       let ctx' = case lp of DnB _ -> extend (All x') ctx\n",
    "                             UpB _ -> extend (Nab x') ctx\n",
    "       return . (and :: [Bool] -> Bool) $ f(ctx',p',q')\n",
    "\n",
    "bisim2' ctx@(nctx,_,_) p q =\n",
    "  do (sigma, r) <- runFreshMT (one_ ctx p)\n",
    "     let (lp, p') = subs_ ctx sigma r\n",
    "     returnL (One nctx (toEqC sigma) lp p') . runFreshMT $ do\n",
    "       (lq, q') <-IdS.one (subs_ ctx sigma q) -- follow with same sub and label\n",
    "       guard $ lp == lq\n",
    "       returnR (One nctx (toEqC sigma) lq q') $ bisim2' ctx p' q'\n",
    "  <|>\n",
    "  do (sigma, r) <- runFreshMT (one_b ctx p)\n",
    "     let (lp, bp') = subs_ ctx sigma r\n",
    "     let x' = runFreshM $ freshFrom (fv nctx) bp' -- to use same new quan var\n",
    "     returnL (OneB nctx (toEqC sigma) lp bp') . runFreshMT $ do\n",
    "       (lq, bq') <-IdS.oneb (subs_ ctx sigma q) -- follow with same sub and label\n",
    "       guard $ lp == lq\n",
    "       (x, p1, q1) <- unbind2' bp' bq'\n",
    "       let x' = x\n",
    "       let (p',q') = (p1,q1)\n",
    "       \n",
    "       let (p', q') | x == x'   = (p1, q1) -- to use same new quan var\n",
    "                    | otherwise = subst x (Var x') (p1, q1)\n",
    "       let ctx' = case lp of DnB _ -> extend (All x') ctx\n",
    "                             UpB _ -> extend (Nab x') ctx\n",
    "       returnR (OneB nctx (toEqC sigma) lq bq') $ bisim2' ctx' p' q'\n",
    "  <|>\n",
    "  do (sigma, r) <- runFreshMT (one_ ctx q)\n",
    "     let (lq, q') = subs_ ctx sigma r\n",
    "     returnR (One nctx (toEqC sigma) lq q') . runFreshMT $ do\n",
    "       (lp, p') <-IdS.one (subs_ ctx sigma p) -- follow with same sub and label\n",
    "       guard $ lp == lq\n",
    "       returnL (One nctx (toEqC sigma) lp p') $ bisim2' ctx p' q'\n",
    "  <|>\n",
    "  do (sigma, r) <- runFreshMT (one_b ctx q)\n",
    "     let (lq, bq') = subs_ ctx sigma r\n",
    "     let x' = runFreshM $ freshFrom (fv nctx) bq' -- to use same new quan var\n",
    "     returnR (OneB nctx (toEqC sigma) lq bq') . runFreshMT $ do\n",
    "       (lp, bp') <-IdS.oneb (subs_ ctx sigma p) -- follow with same sub and label\n",
    "       guard $ lp == lq\n",
    "       (x, q1, p1) <- unbind2' bq' bp'\n",
    "       let (p',q') = (p1,q1)\n",
    "       let (p', q') | x == x'   = (p1, q1) -- to use same new quan var\n",
    "                    | otherwise = subst x (Var x') (p1, q1)\n",
    "       let ctx' = case lp of DnB _ -> extend (All x') ctx\n",
    "                             UpB _ -> extend (Nab x') ctx\n",
    "       returnL (OneB nctx (toEqC sigma) lp bp') $ bisim2' ctx' p' q'\n",
    "  where toEqC = part2eqc ctx\n",
    "\n",
    "freshFrom :: Fresh m => [Nm] -> PrB -> m Nm\n",
    "freshFrom xs b = do { mapM_ fresh xs; fst <$> unbind b }\n",
    "\n",
    "forest2df :: [Tree (Either StepLog StepLog)] -> [(Form,Form)]\n",
    "forest2df rs\n",
    "            =    do  Node (Left (One _ sigma_p a _)) [] <- rs\n",
    "                     let sigmaqs = subsMatchingAct a (right1s rs)\n",
    "                     return (prebase sigma_p a, postbase sigmaqs a)\n",
    "            <|>  do  Node (Right (One _ sigma_q a _)) [] <- rs\n",
    "                     let formR = prebase sigma_q a\n",
    "                     let sigmaps = subsMatchingAct a (left1s rs)\n",
    "                     return (postbase sigmaps a, formR)\n",
    "            <|>  do  Node (Left (OneB _ sigma_p a _)) [] <- rs\n",
    "                     let sigmaqs = subsMatchingActB a (right1Bs rs)\n",
    "                     return (preBbase sigma_p a, postBbase sigmaqs a)\n",
    "            <|>  do  Node (Right (OneB _ sigma_q a _)) [] <- rs\n",
    "                     let formR = preBbase sigma_q a\n",
    "                     let sigmaps = subsMatchingActB a (left1Bs rs)\n",
    "                     return (postBbase sigmaps a, formR)\n",
    "            <|>  do  Node (Left (One _ sigma_p a _)) rsR <- rs\n",
    "                     let rss' = [rs' | Node _ rs' <- rsR]\n",
    "                     (dfsL,dfsR) <- unzip <$> sequence (forest2df <$> rss')\n",
    "                     guard . not . null $ dfsL\n",
    "                     let sigmaqs = subsMatchingAct a (right1s rs)\n",
    "                     return (pre sigma_p a dfsL, post sigmaqs a dfsR)\n",
    "            <|>  do  Node (Right (One _ sigma_q a _)) rsL <- rs\n",
    "                     let rss' = [rs' | Node _ rs' <- rsL]\n",
    "                     (dfsL,dfsR) <- unzip <$> sequence (forest2df <$> rss')\n",
    "                     guard . not . null $ dfsL\n",
    "                     let sigmaps = subsMatchingAct a (left1s rs)\n",
    "                     return (post sigmaps a dfsL, pre sigma_q a dfsR)\n",
    "            <|>  do  Node (Left (OneB nctx sigma_p a _)) rsR <- rs\n",
    "                     let  rss' = [rs' | Node _ rs' <- rsR]\n",
    "                          x = quan2nm . head . getCtx . fromEither\n",
    "                            . rootLabel . head $ head rss'\n",
    "                     (dfsL,dfsR) <- unzip <$> sequence (forest2df <$> rss')\n",
    "                     guard . not . null $ dfsL\n",
    "                     let sigmaqs = subsMatchingActB a (right1Bs rs)\n",
    "                     return (preB sigma_p a x dfsL, postB sigmaqs a x dfsR)\n",
    "            <|>  do  Node (Right (OneB nctx sigma_q a _)) rsL <- rs\n",
    "                     let  rss' = [rs' | Node _ rs' <- rsL]\n",
    "                          x = quan2nm . head . getCtx . fromEither . rootLabel\n",
    "                                $ head (head rss')\n",
    "                     (dfsL,dfsR) <- unzip <$> sequence (forest2df <$> rss')\n",
    "                     guard . not . null $ dfsL\n",
    "                     let sigmaps = subsMatchingActB a (left1Bs rs)\n",
    "                     return (postB sigmaps a x dfsL, preB sigma_q a x dfsR)\n",
    "  where\n",
    "    prebase sigma a = pre sigma a []\n",
    "    postbase sigmas a = post sigmas a []\n",
    "    preBbase sigma a = preB sigma a (s2n \"?\") []\n",
    "    postBbase sigmas a = postB sigmas a (s2n \"?\") []\n",
    "    pre sigma a = boxMat sigma . Dia a . conj\n",
    "    post sigmas a fs = Box a . disj $  (diaMat<$>sigmas) ++ fs\n",
    "    preB sigma a x = boxMat sigma . DiaB a . bind x . conj\n",
    "    postB sigmas a x fs = BoxB a . bind x . disj $  (diaMat<$>sigmas) ++ fs\n",
    "    boxMat  [] = id; boxMat  sigma = BoxMatch [(Var x,Var y) | (x,y)<-sigma]\n",
    "    diaMat  [] = FF; diaMat  sigma = DiaMatch [(Var x,Var y) | (x,y)<-sigma]\n",
    "    right1s  rs = [log | Node (Right  log@One{}) _ <- rs]\n",
    "    left1s   rs = [log | Node (Left   log@One{}) _ <- rs]\n",
    "    right1Bs  rs = [log | Node (Right  log@OneB{}) _ <- rs]\n",
    "    left1Bs   rs = [log | Node (Left   log@OneB{}) _ <- rs]\n",
    "    getCtx (One   nctx _ _ _)  = nctx; getCtx (OneB  nctx _ _ _) = nctx\n",
    "    fromEither (Left   t) = t; fromEither (Right  t) = t\n",
    "\n",
    "subsMatchingAct :: Act -> [StepLog] -> [EqC]\n",
    "subsMatchingAct a logs =\n",
    "  do  One nctx sigma a' _ <-logs          ;  let sigmaSubs = subs nctx sigma\n",
    "      guard $ sigmaSubs a == sigmaSubs a' ;  return sigma\n",
    "\n",
    "subsMatchingActB :: ActB -> [StepLog] -> [EqC]\n",
    "subsMatchingActB a logs =\n",
    "  do  OneB nctx sigma a' _ <-logs         ;  let sigmaSubs = subs nctx sigma\n",
    "      guard $ sigmaSubs a == sigmaSubs a' ;  return sigma"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Examples"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "{-# LANGUAGE FlexibleContexts          #-}\n",
    "{-# LANGUAGE FlexibleInstances         #-}\n",
    "{-# LANGUAGE MultiParamTypeClasses     #-}\n",
    "{-# LANGUAGE NoMonomorphismRestriction #-}\n",
    "{-# LANGUAGE ScopedTypeVariables       #-}\n",
    "{-# LANGUAGE UndecidableInstances      #-}\n",
    "module PP where\n",
    "\n",
    "import Prelude hiding ((<>))\n",
    "\n",
    "import           Data.Tree hiding (drawTree, drawForest)\n",
    "import           Data.Tree.View hiding (drawTree)\n",
    "import qualified IdSubLTS                       as IdS\n",
    "import           OpenBisim\n",
    "import qualified OpenLTS                        as OpS\n",
    "import           OpenLTS\n",
    "import           PiCalc\n",
    "import           Text.PrettyPrint\n",
    "import           Text.PrettyPrint.HughesPJClass\n",
    "import           Unbound.Generics.LocallyNameless\n",
    "\n",
    "import IHaskell.Display\n",
    "import Data.List (intersperse)\n",
    "\n",
    "appPrec :: Rational\n",
    "appPrec = 10\n",
    "\n",
    "pp = print . pPrint\n",
    "ppTeX = html . texParen . ppTeXstring\n",
    "\n",
    "pPrintTeX = pPrint . TeX\n",
    "ppTeXstring = show . pPrintTeX\n",
    "texParen s = \"$\"++s++\"$\"\n",
    "\n",
    "instance Pretty Nm where pPrint = text . show\n",
    "\n",
    "instance Pretty Quan where\n",
    "  pPrintPrec l r (All x) = maybeParens (r > appPrec) $ text \"All\" <+> ppp x\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (Nab x) = maybeParens (r > appPrec) $ text \"Nab\" <+> ppp x\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "    \n",
    "instance (Alpha a, Pretty a) => Pretty (Bind Nm a) where\n",
    "  pPrintPrec l r b = maybeParens (r > appPrec) $ ppp x <+> text \".\\\\\" <+> ppp p\n",
    "    where ppp = pPrintPrec l (appPrec+1); (x,p) = runFreshM $ unbind b\n",
    "\n",
    "instance Pretty Tm where\n",
    "  pPrintPrec l r (Var x) = maybeParens (r > appPrec) $ text \"Var\" <+> ppp x\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "\n",
    "instance Pretty Pr where\n",
    "  pPrintPrec _ _ Null = text \"Null\"\n",
    "  pPrintPrec l r (TauP p) = maybeParens (r > appPrec) $\n",
    "            text \"TauP\" <+> ppp p\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (Out x y p) = maybeParens (r > appPrec) $\n",
    "            text \"Out\" <+> ppp x <+> ppp y <+> ppp p\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (In x b) = maybeParens (r > appPrec) $\n",
    "            text \"In\" <+> ppp x <+> ppp b\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (Plus p q) = maybeParens (r > appPrec) $\n",
    "            ppp p <+> text \"`Plus`\" <+> ppp q\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (Par p q) = maybeParens (r > appPrec) $\n",
    "            ppp p <+> text \"`Par`\" <+> ppp q\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (Nu b) = maybeParens (r > appPrec) $\n",
    "            text \"Nu\" <> ppp b\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (Match x y p) = maybeParens (r > appPrec) $\n",
    "            text \"Match\" <+> ppp x <+> ppp y <+> ppp p\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "    \n",
    "\n",
    "newtype TeX a = TeX a deriving Show\n",
    "\n",
    "instance (Alpha a, Pretty (TeX a)) => Pretty (TeX(Bind Nm a)) where\n",
    "  pPrintPrec l r (TeX b) = maybeParens (r > appPrec) $\n",
    "            text \"(\" <+> ppp x <+> text \").\\\\!\" <+> ppp p\n",
    "    where ppp = pPrintPrec l appPrec . TeX; (x,p) = runFreshM $ unbind b\n",
    "\n",
    "instance Pretty (TeX Nm) where -- assume that we always show free names (Fn{}) only\n",
    "  pPrintPrec l r (TeX x) = case n of 0 -> text $ s\n",
    "                                     _ -> text $ s++\"_{\"++show n++\"}\"\n",
    "    where s = name2String x\n",
    "          n = name2Integer x\n",
    "\n",
    "instance Pretty (TeX Tm) where\n",
    "  pPrintPrec l r (TeX (Var x)) = pPrintPrec l r x\n",
    "\n",
    "\n",
    "plusPrec, parPrec:: Rational\n",
    "plusPrec = 5\n",
    "parPrec = 6\n",
    "\n",
    "instance Pretty (TeX Pr) where\n",
    "  pPrintPrec _ _ (TeX Null) = text \"0\"\n",
    "  pPrintPrec l r (TeX(TauP p)) = maybeParens (r > appPrec) $\n",
    "            text \"\\\\tau\\\\!.\\\\!\" <+> ppp p\n",
    "    where ppp = pPrintPrec l appPrec . TeX\n",
    "  pPrintPrec l r (TeX(Out x y p)) = maybeParens (r > appPrec) $\n",
    "            text \"\\\\overline\" <+> ppp x <+> ppp y <+> text \".\\\\!\" <+> ppp p\n",
    "    where ppp = pPrintPrec l appPrec . TeX\n",
    "  pPrintPrec l r (TeX(In x b)) = maybeParens (r > appPrec) $\n",
    "            ppp x <+> ppp b\n",
    "    where ppp = pPrintPrec l appPrec . TeX\n",
    "  pPrintPrec l r (TeX(Plus p q)) = maybeParens (r > plusPrec) $\n",
    "            ppp p <+> text \"+\" <+> ppp q\n",
    "    where ppp = pPrintPrec l plusPrec . TeX\n",
    "  pPrintPrec l r (TeX(Par p q)) = maybeParens (r > parPrec) $\n",
    "            ppp p <+> text \"\\\\mid{}\" <+> ppp q\n",
    "    where ppp = pPrintPrec l parPrec . TeX\n",
    "  pPrintPrec l r (TeX(Nu b)) = maybeParens (r > appPrec) $\n",
    "            text \"\\\\nu\" <+> ppp x <+> text \".\\\\!\" <+> ppp p\n",
    "    where ppp = pPrintPrec l appPrec . TeX; (x,p) = runFreshM $ unbind b\n",
    "  pPrintPrec l r (TeX(Match x y p)) = maybeParens (r > appPrec) $\n",
    "            text \"[\" <+> ppp x <+> text \"=\" <+> ppp y <+> text \"]\" <+> ppp p\n",
    "    where ppp = pPrintPrec l appPrec . TeX\n",
    "\n",
    "\n",
    "instance Pretty Act where\n",
    "  pPrintPrec l r (Up x y) = maybeParens (r > appPrec) $ text \"Up\" <+> ppp x <+> ppp y\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r Tau = text \"Tau\"\n",
    "instance Pretty ActB where\n",
    "  pPrintPrec l r (UpB x) = maybeParens (r > appPrec) $ text \"UpB\" <+> ppp x\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (DnB x) = maybeParens (r > appPrec) $ text \"DnB\" <+> ppp x\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "\n",
    "instance Pretty Form where\n",
    "  pPrintPrec _ _ FF = text \"FF\"\n",
    "  pPrintPrec _ _ TT = text \"TT\"\n",
    "  pPrintPrec l r (Conj fs) = maybeParens (r > appPrec) $\n",
    "            text \"Conj\" <> ppp fs\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (Disj fs) = maybeParens (r > appPrec) $\n",
    "            text \"Disj\" <> ppp fs\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (Box a f) = maybeParens (r > appPrec) $\n",
    "            text \"Box\" <+> ppp a <+> ppp f\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (Dia a f) = maybeParens (r > appPrec) $\n",
    "             text \"Dia\" <+> ppp a <+> ppp f\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (BoxB a f) = maybeParens (r > appPrec) $\n",
    "            text \"BoxB\" <+> ppp a <+> ppp f\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (DiaB a f) = maybeParens (r > appPrec) $\n",
    "            text \"DiaB\" <+> ppp a <+> ppp f\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (BoxMatch sigma f) = maybeParens (r > appPrec) $\n",
    "            text \"BoxMatch\" <+> ppp sigma <+> ppp f\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (DiaMatch sigma) = maybeParens (r > appPrec) $\n",
    "            text \"DiaMatch\" <+> ppp sigma\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "    \n",
    "instance Pretty StepLog where\n",
    "  pPrintPrec l r (One  nctx sigma a p) = maybeParens (r > appPrec) $\n",
    "            text \"One\" <+> ppp nctx <+> ppp sigma <+> ppp a <+> ppp p\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "  pPrintPrec l r (OneB nctx sigma a b) = maybeParens (r > appPrec) $\n",
    "            text \"OneB\" <+> ppp nctx <+> ppp sigma <+> ppp a <+> ppp b\n",
    "    where ppp = pPrintPrec l (appPrec+1)\n",
    "    \n",
    "    \n",
    "    \n",
    "instance Pretty (TeX Act) where\n",
    "  pPrintPrec l r (TeX(Up x y)) = maybeParens (r > appPrec) $\n",
    "            text \"\\\\overline{\" <+> ppp x <+> text \"}\" <+> ppp y\n",
    "    where ppp = pPrintPrec l (appPrec+1) . TeX\n",
    "  pPrintPrec l r (TeX Tau) = text \"\\\\tau\"\n",
    "instance Pretty (TeX ActB) where\n",
    "  pPrintPrec l r (TeX(UpB x)) = maybeParens (r > appPrec) $ text \"\\\\overline{\" <+> ppp x <+> text \"}\"\n",
    "    where ppp = pPrintPrec l (appPrec+1) . TeX\n",
    "  pPrintPrec l r (TeX(DnB x)) = maybeParens (r > appPrec) $ ppp x\n",
    "    where ppp = pPrintPrec l (appPrec+1) . TeX\n",
    "\n",
    "conjPrec, disjPrec :: Rational\n",
    "conjPrec = 6\n",
    "disjPrec = 5\n",
    "\n",
    "\n",
    "instance Pretty (TeX Form) where\n",
    "  pPrintPrec _ _ (TeX FF) = text \"\\\\bot{}\"\n",
    "  pPrintPrec _ _ (TeX TT) = text \"\\\\top{}\"\n",
    "  pPrintPrec l r (TeX(Conj [])) = ppp TT\n",
    "    where ppp = pPrintPrec l conjPrec . TeX  \n",
    "  pPrintPrec l r (TeX(Conj fs)) = maybeParens (r > conjPrec) $\n",
    "            foldr1 (<+>) . intersperse (text \"\\\\land{}\") $ map ppp fs\n",
    "    where ppp = pPrintPrec l conjPrec . TeX\n",
    "  pPrintPrec l r (TeX(Disj [])) = ppp FF\n",
    "    where ppp = pPrintPrec l disjPrec . TeX\n",
    "  pPrintPrec l r (TeX(Disj fs)) = maybeParens (r > disjPrec) $\n",
    "            foldr1 (<+>) . intersperse (text \"\\\\lor{}\") $ map ppp fs\n",
    "    where ppp = pPrintPrec l disjPrec . TeX\n",
    "  pPrintPrec l r (TeX(Box a f)) = maybeParens (r > appPrec) $\n",
    "            text \"[\" <+> ppp a <+> text \"]\" <+> ppp f\n",
    "    where ppp = pPrintPrec l appPrec . TeX\n",
    "  pPrintPrec l r (TeX(Dia a f)) = maybeParens (r > appPrec) $\n",
    "             text \"\\\\langle{}\" <+> ppp a <+> text \"\\\\rangle{}\" <+> ppp f\n",
    "    where ppp = pPrintPrec l appPrec . TeX\n",
    "  pPrintPrec l r (TeX(BoxB a b)) = maybeParens (r > appPrec) $\n",
    "            text \"[\" <+> ppp a <+> text \"(\" <+> ppp x <+> text \")]\" <+> ppp f\n",
    "    where ppp = pPrintPrec l appPrec . TeX\n",
    "          (x,f) = runFreshM $ unbind b\n",
    "  pPrintPrec l r (TeX(DiaB a b)) = maybeParens (r > appPrec) $\n",
    "            text \"\\\\langle{}\" <+> ppp a <+> text \"(\" <+> ppp x <+> text \")\\\\rangle{}\" <+> ppp f\n",
    "    where ppp = pPrintPrec l appPrec . TeX\n",
    "          (x,f) = runFreshM $ unbind b\n",
    "  pPrintPrec l r (TeX(BoxMatch [] f)) = ppp f\n",
    "    where ppp = pPrintPrec l appPrec . TeX\n",
    "  pPrintPrec l r (TeX(BoxMatch sigma f)) = maybeParens (r > appPrec) $\n",
    "            text \"[\" <+> foldr1 (<+>) [ppp x <+> text \"=\" <+> ppp y | (x,y)<-sigma]\n",
    "        <+> text \"]\" <+> ppp f\n",
    "    where ppp = pPrintPrec l appPrec . TeX\n",
    "  pPrintPrec l r (TeX(DiaMatch [])) = ppp FF\n",
    "    where ppp = pPrintPrec l appPrec . TeX\n",
    "  pPrintPrec l r (TeX(DiaMatch sigma)) = maybeParens (r > disjPrec) $\n",
    "            foldr1 (<+>) $ intersperse (text \"\\\\lor{}\") [ppp x <+> text \"=\" <+> ppp y | (x,y)<-sigma]\n",
    "    where ppp = pPrintPrec l appPrec . TeX\n",
    "\n",
    "instance Pretty (TeX StepLog) where\n",
    "  pPrintPrec l r (TeX(One  nctx sigma a p)) = -- maybeParens (r > appPrec) $\n",
    "            text \"h=\" <+> texHistory nctx <+> text \",\\\\,\\\\sigma=\" <+> ppp sigma <+> text \"\\\\quad\"\n",
    "        <+> text \"{-}\" <+> tex a <+> text \"{\\\\rightarrow{}}~~\" <+> tex p\n",
    "    where ppp = pPrintPrec l 0; tex = ppp . TeX\n",
    "  pPrintPrec l r (TeX(OneB nctx sigma a b)) = -- maybeParens (r > appPrec) $\n",
    "            text \"h=\" <+> texHistory nctx <+> text \",\\\\,\\\\sigma=\" <+> ppp sigma <+> text \"\\\\quad\"\n",
    "        <+> text \"{-}\" <+> tex a <+> text \"(\\\\cdot){\\\\rightarrow{}}~~\" <+> tex b\n",
    "    where ppp = pPrintPrec l 0; tex = ppp . TeX\n",
    "\n",
    "texHistory [] = empty\n",
    "texHistory h  = foldr1 (<+>) . intersperse (text \"\\\\!\\\\!\\\\cdot\\\\!\") . reverse $ map texHistoryItem h \n",
    "texHistoryItem (All x) = text $ show x++\"^i\"\n",
    "texHistoryItem (Nab y) = text $ show y++\"^o\"\n",
    "\n",
    "drawTree = showTree . toTreeString\n",
    "drawForest = unlines . map drawTree\n",
    "\n",
    "texTree = myHtmlTree . toTreeTeX\n",
    "texForest = unlines . map texTree\n",
    "\n",
    "myHtmlTree = show . tree2html\n",
    "\n",
    "tree2html (Node l ns) = ul . foldr1 (<+>) $ (li . label $ text l) : map tree2html ns\n",
    "  where\n",
    "  tag t Nothing content = text(\"<\"++t++\">\") <+> content <+> text(\"</\"++t++\">\")\n",
    "  tag t (Just s) content = text(\"<\"++t++\" \"++s++\">\") <+> content <+> text(\"</\"++t++\">\")\n",
    "  ul = tag \"ul\" (Just \"class='nested'\")\n",
    "  li = tag \"li\" Nothing\n",
    "  label = tag \"label\" Nothing\n",
    "\n",
    "\n",
    "render1line = renderStyle style{mode=OneLineMode}\n",
    "\n",
    "toTreeString = foldTree (\\log ts -> Node (render1line . pPrint $ log) ts)\n",
    "toTreeTeX = foldTree (\\log ts -> Node (texParen . render1line . eitherTeX $ log) ts)\n",
    "  where eitherTeX (Left x) = text \"\\\\color{blue}{\\\\mathsf{L}\\\\!:\" <+> pPrintTeX x <+> text \"}\"\n",
    "        eitherTeX (Right y) = text \"\\\\color{red}{\\\\mathsf{R}\\\\!:\" <+> pPrintTeX y <+> text \"}\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [],
   "source": [
    "import qualified IdSubLTS                       as IdS\n",
    "import           OpenBisim\n",
    "import qualified OpenLTS                        as OpS\n",
    "import           OpenLTS\n",
    "import           PiCalc\n",
    "import           Text.PrettyPrint\n",
    "import           Text.PrettyPrint.HughesPJClass\n",
    "import           Unbound.Generics.LocallyNameless\n",
    "import PP\n",
    "\n",
    "x, y, z :: Nm\n",
    "w = s2n \"w\"\n",
    "x = s2n \"x\"\n",
    "y = s2n \"y\"\n",
    "z = s2n \"z\"\n",
    "\n",
    "q1 = taup q2\n",
    "q2 = (x.= y)(taup o)\n",
    "\n",
    "p1 = tau .+ taup tau\n",
    "p2 = inp x(z.\\out x z o) .| out x y o\n",
    "p3 = inp x(z.\\out x z o) .| out y x o\n",
    "\n",
    "axay = reverse [All x, All y]\n",
    "axny = reverse [All x, Nab y]\n",
    "nxay = reverse [Nab x, All y]\n",
    "nxny = reverse [Nab x, Nab y]\n",
    "axayazaw = reverse $ map All [x,y,z,w]\n",
    "\n",
    "printLateOneFrom p = do\n",
    "  putStrLn $ \"one step from: \" ++ render1line (pPrint p)\n",
    "  mapM_ pp (runFreshMT (IdS.one p) :: [(Act,Pr)])\n",
    "\n",
    "\n",
    "printOpenOneFrom nctx p = do\n",
    "  putStrLn $ \"one step from: \" ++ show (reverse nctx) ++ \" \"++ render1line (pPrint p)\n",
    "  mapM_ pp (runFreshMT (OpS.one nctx p) :: [([(Nm,Nm)],(Act,Pr))])\n",
    "\n",
    "\n",
    "axayaaab = map All [x,y,a,b]\n",
    "a = s2n \"a\"\n",
    "b = s2n \"b\"\n",
    "\n",
    "ppp1 = taup(out a a o .+out b b o) .+ (x.= y) (taup $ out a a o)\n",
    "qqq1 = taup(out a a o .+out b b o) .+ taup (out a a o)\n",
    "\n",
    "ppp2 = nu$x.\\out a x (inp a $y.\\tau)\n",
    "qqq2 = nu$x.\\out a x (inp a $y.\\(x.= y) tau)\n",
    "\n",
    "t_tt = tau .+ taup tau\n",
    "\n",
    "dosomething = do\n",
    "  (s,(l,p')) <- OpS.one nctx p\n",
    "  return $ subs nctx s p'\n",
    "  where\n",
    "  nctx = axayazaw\n",
    "  p =\n",
    "      (x.= w) . (z.= x) $\n",
    "      -- (x.= y) . (w.= z) $\n",
    "      taup (out x w o) .+ taup (out y z o)\n",
    "\n",
    "dosomething2 = do\n",
    "  (s,(l,bp')) <- OpS.oneb nctx p\n",
    "  return $ subs nctx s bp'\n",
    "  where\n",
    "    nctx = []\n",
    "    p = Nu$x.\\(inp x$y.\\taup o)\n",
    "\n",
    "dosomething3 = do\n",
    "  (s,(l,bp')) <- OpS.oneb nctx p\n",
    "  return $ subs nctx s bp'\n",
    "  where\n",
    "    nctx = [All a]\n",
    "    p = Nu$x.\\ out a x o\n",
    "\n",
    "dosomething4 = do\n",
    "  (s,(l,p')) <- OpS.one nctx p\n",
    "  return $ subs nctx s p'\n",
    "  where\n",
    "    nctx = [All a]\n",
    "    p = Nu$x.\\ out a x o\n",
    "\n",
    "dosomething5 = do\n",
    "  (s,(l,bp')) <- OpS.oneb nctx p\n",
    "  return $ subs nctx s bp'\n",
    "  where\n",
    "    nctx = [All a]\n",
    "    p = Nu$x.\\ out x a o"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Late LTS"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "one step from: (TauP Null) `Plus` (TauP (TauP Null))\n",
       "(Tau, Null)\n",
       "(Tau, TauP Null)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "printLateOneFrom p1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "one step from: TauP (Match (Var x) (Var y) (TauP Null))\n",
       "(Tau, Match (Var x) (Var y) (TauP Null))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "printLateOneFrom q1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "one step from: Match (Var x) (Var y) (TauP Null)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "printLateOneFrom q2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "one step from: (In (Var x) (z .\\ (Out (Var x) (Var z) Null))) `Par` (Out (Var x) (Var y) Null)\n",
       "(Up (Var x) (Var y),\n",
       " (In (Var x) (z .\\ (Out (Var x) (Var z) Null))) `Par` Null)\n",
       "(Tau, (Out (Var x) (Var y) Null) `Par` Null)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "printLateOneFrom p2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "one step from: (In (Var x) (z .\\ (Out (Var x) (Var z) Null))) `Par` (Out (Var y) (Var x) Null)\n",
       "(Up (Var y) (Var x),\n",
       " (In (Var x) (z .\\ (Out (Var x) (Var z) Null))) `Par` Null)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "printLateOneFrom p3"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Open LTS"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "one step from: [All x,All y] (TauP Null) `Plus` (TauP (TauP Null))\n",
       "([], (Tau, Null))\n",
       "([], (Tau, TauP Null))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "printOpenOneFrom axay p1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "one step from: [All x,All y] TauP (Match (Var x) (Var y) (TauP Null))\n",
       "([], (Tau, Match (Var x) (Var y) (TauP Null)))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "printOpenOneFrom axay q1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "one step from: [All x,All y] Match (Var x) (Var y) (TauP Null)\n",
       "([(y, x)], (Tau, Null))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "printOpenOneFrom axay q2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "one step from: [All x,Nab y] Match (Var x) (Var y) (TauP Null)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "printOpenOneFrom axny q2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "one step from: [Nab x,All y] Match (Var x) (Var y) (TauP Null)\n",
       "([(y, x)], (Tau, Null))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "printOpenOneFrom nxay q2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "one step from: [Nab x,Nab y] Match (Var x) (Var y) (TauP Null)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "printOpenOneFrom nxny q2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "one step from: [All x,All y] (In (Var x) (z .\\ (Out (Var x) (Var z) Null))) `Par` (Out (Var x) (Var y) Null)\n",
       "([],\n",
       " (Up (Var x) (Var y),\n",
       "  (In (Var x) (z .\\ (Out (Var x) (Var z) Null))) `Par` Null))\n",
       "([], (Tau, (Out (Var x) (Var y) Null) `Par` Null))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "printOpenOneFrom axay p2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "one step from: [All x,All y] (In (Var x) (z .\\ (Out (Var x) (Var z) Null))) `Par` (Out (Var y) (Var x) Null)\n",
       "([],\n",
       " (Up (Var y) (Var x),\n",
       "  (In (Var x) (z .\\ (Out (Var x) (Var z) Null))) `Par` Null))\n",
       "([(y, x)], (Tau, (Out (Var x) (Var x) Null) `Par` Null))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "printOpenOneFrom axay p3"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[Out (Var x) (Var x) Null,Out (Var y) (Var x) Null]"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "runFreshMT dosomething :: [Pr]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$h= x^i \\!\\!\\cdot\\! y^i$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\!: \\tau\\!.\\! 0 + \\tau\\!.\\! \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{R}\\!: \\tau\\!.\\! [ x = y ] \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "Left (One [All y, All x] [] Tau Null)\n",
       " └╴Right (One [All y, All x] [] Tau (Match (Var x) (Var y) (TauP Null)))\n",
       "    └╴Right (One [All y, All x] [(y, x)] Tau Null)\n",
       "\n",
       "Left (One [All y, All x] [] Tau (TauP Null))\n",
       " └╴Right (One [All y, All x] [] Tau (Match (Var x) (Var y) (TauP Null)))\n",
       "    ├╴Left (One [All y, All x] [] Tau Null)\n",
       "    └╴Right (One [All y, All x] [(y, x)] Tau Null)\n",
       "       └╴Left (One [All y, All x] [(y, x)] Tau Null)\n",
       "\n",
       "Right (One [All y, All x] [] Tau (Match (Var x) (Var y) (TauP Null)))\n",
       " ├╴Left (One [All y, All x] [] Tau Null)\n",
       " │  └╴Right (One [All y, All x] [(y, x)] Tau Null)\n",
       " └╴Left (One [All y, All x] [] Tau (TauP Null))\n",
       "    ├╴Left (One [All y, All x] [] Tau Null)\n",
       "    └╴Right (One [All y, All x] [(y, x)] Tau Null)\n",
       "       └╴Left (One [All y, All x] [(y, x)] Tau Null)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ [ x = y ] \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [(y, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul>\n",
       "<ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ [ x = y ] \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [(y, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [(y, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul> </ul>\n",
       "<ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ [ x = y ] \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [(y, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [(y, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [(y, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul> </ul>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "(Dia Tau (Box Tau FF),Box Tau (BoxMatch [(Var y,Var x)] (Dia Tau TT)))\n",
       "(Dia Tau (Dia Tau TT),Box Tau (Box Tau (DiaMatch [(Var y,Var x)])))\n",
       "(Box Tau (Disj [Box Tau FF,Dia Tau TT]),Dia Tau (Conj [BoxMatch [(Var y,Var x)] (Dia Tau TT),Box Tau (DiaMatch [(Var y,Var x)])]))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\langle{} \\tau \\rangle{} [ \\tau ] \\bot{}~,~~[ \\tau ] [ y = x ] \\langle{} \\tau \\rangle{} \\top{}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\langle{} \\tau \\rangle{} \\langle{} \\tau \\rangle{} \\top{}~,~~[ \\tau ] [ \\tau ] (y = x)$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$[ \\tau ] ([ \\tau ] \\bot{} \\lor{} \\langle{} \\tau \\rangle{} \\top{})~,~~\\langle{} \\tau \\rangle{} ([ y = x ] \\langle{} \\tau \\rangle{} \\top{} \\land{} [ \\tau ] (y = x))$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "import IHaskell.Display\n",
    "\n",
    "map (html . texParen . show)\n",
    "  [ text \"h=\"<+> texHistory axay\n",
    "  , text \"\\\\mathsf{L}\\\\!:\" <+> pPrintTeX (tau .+ taup tau)\n",
    "  , text \"\\\\mathsf{R}\\\\!:\" <+> pPrintTeX (TauP $ (x.= y)tau)\n",
    "  ]\n",
    "\n",
    "bisim axay (tau .+ taup tau) (taup $ (x.= y)tau)\n",
    "putStrLn . drawForest $ bisim' axay (tau .+ taup tau) (taup $ (x.= y) tau)\n",
    "\n",
    "html . texForest $ bisim' axay (tau .+ taup tau) (taup $ (x.= y) tau)\n",
    "\n",
    "mapM_ print . forest2df $ bisim' axay (tau .+ taup tau) (taup $ (x.= y) tau)\n",
    "\n",
    "map (\\(f1,f2) -> html . texParen $ ppTeXstring f1++\"~,~~\"++ppTeXstring f2 )\n",
    "            . forest2df $ bisim' axay (tau .+ taup tau) (taup $ (x.= y) tau)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [],
   "source": [
    "-- runBisimExperiment history leftProces rightProcess\n",
    "runBisimExperiment h prL prR =\n",
    "  sequence . map (display . html) $\n",
    "        map (texParen . show)\n",
    "            [ text \"h=\"<+> texHistory h\n",
    "            , text \"\\\\mathsf{L}\\\\!:\" <+> pPrintTeX prL\n",
    "            , text \"\\\\mathsf{R}\\\\!:\" <+> pPrintTeX prR\n",
    "            , text $ \"\\\\mathsf{L}\"\n",
    "                ++ (if bisimResult then \"\\\\sim\" else \"\\\\not\\\\sim\")\n",
    "                ++ \"\\\\mathsf{R}\"\n",
    "                ++ \"\\\\qquad{}\\\\text{\" ++ (if bisimResult then \"\" else \"non-\") ++ \"bisimilar}\"\n",
    "            ]\n",
    "    ++ [ texParen $ \"\\\\phi_L=\"++ppTeXstring fL++\"\\\\;,~~\\\\phi_R=\"++ppTeXstring fR\n",
    "                                        | (fL,fR) <- forest2df bisimForest ]\n",
    "    ++ [ texForest bisimForest ] -- ++ [ \"<pre>\"++ drawForest bisimForest ++\"</pre>\" ]\n",
    "  where\n",
    "   bisimResult = bisim h prL prR\n",
    "   bisimForest = bisim' h prL prR"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\!: \\overline x a .\\! \\overline x b .\\! 0 + \\overline x a .\\! (\\overline x b .\\! 0 + \\overline x c .\\! 0)$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{R}\\!: \\overline x a .\\! (\\overline x b .\\! 0 + \\overline x c .\\! 0)$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\not\\sim\\mathsf{R}\\qquad{}\\text{non-bisimilar}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\phi_L=\\langle{} \\overline{ x } a \\rangle{} [ \\overline{ x } c ] \\bot{}\\;,~~\\phi_R=[ \\overline{ x } a ] \\langle{} \\overline{ x } c \\rangle{} \\top{}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } a {\\rightarrow{}}~~ \\overline x b .\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } a {\\rightarrow{}}~~ \\overline x b .\\! 0 + \\overline x c .\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } c {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul>\n",
       "<ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } a {\\rightarrow{}}~~ \\overline x b .\\! 0 + \\overline x c .\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } a {\\rightarrow{}}~~ \\overline x b .\\! 0 + \\overline x c .\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } c {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } c {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } c {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } c {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul> </ul>\n",
       "<ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } a {\\rightarrow{}}~~ \\overline x b .\\! 0 + \\overline x c .\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } a {\\rightarrow{}}~~ \\overline x b .\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } c {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } a {\\rightarrow{}}~~ \\overline x b .\\! 0 + \\overline x c .\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } c {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } c {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } b {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } c {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= c^i \\!\\!\\cdot\\! b^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\overline{ x } c {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul> </ul>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "x = s2n \"x\"\n",
    "a = s2n \"a\"\n",
    "b = s2n \"b\"\n",
    "c = s2n \"c\"\n",
    "runBisimExperiment [All x,All a,All b,All c]\n",
    "   (out x a (out x b o) .+ out x a (out x b o .+ out x c o))\n",
    "   (out x a (out x b o .+ out x c o))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$h= y^i \\!\\!\\cdot\\! x^i$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\!: \\tau\\!.\\! 0 + \\tau\\!.\\! \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{R}\\!: \\tau\\!.\\! [ x = y ] \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\not\\sim\\mathsf{R}\\qquad{}\\text{non-bisimilar}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\phi_L=\\langle{} \\tau \\rangle{} [ \\tau ] \\bot{}\\;,~~\\phi_R=[ \\tau ] [ x = y ] \\langle{} \\tau \\rangle{} \\top{}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\phi_L=\\langle{} \\tau \\rangle{} \\langle{} \\tau \\rangle{} \\top{}\\;,~~\\phi_R=[ \\tau ] [ \\tau ] (x = y)$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\phi_L=[ \\tau ] ([ \\tau ] \\bot{} \\lor{} \\langle{} \\tau \\rangle{} \\top{})\\;,~~\\phi_R=\\langle{} \\tau \\rangle{} ([ x = y ] \\langle{} \\tau \\rangle{} \\top{} \\land{} [ \\tau ] (x = y))$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ [ x = y ] \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [(x, y)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul>\n",
       "<ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ [ x = y ] \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [(x, y)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [(x, y)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul> </ul>\n",
       "<ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ [ x = y ] \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [(x, y)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [(x, y)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= y^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [(x, y)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul> </ul>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "-- runBisimExperiment history leftProces rightProcess\n",
    "x = s2n \"x\"\n",
    "y = s2n \"y\"\n",
    "runBisimExperiment [All x, All y] (tau .+ taup tau) (taup $ (x.= y) tau)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$h= a^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! x^i$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\!: [ x = k ] \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{R}\\!: \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\not\\sim\\mathsf{R}\\qquad{}\\text{non-bisimilar}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\phi_L=[ \\tau ] (x = k)\\;,~~\\phi_R=\\langle{} \\tau \\rangle{} \\top{}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= a^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [(x, k)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= a^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [(x, k)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul>\n",
       "<ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= a^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "k = s2n \"k\"\n",
    "runBisimExperiment [All x,All k,All a]\n",
    "  ((x.=k)tau)\n",
    "  tau"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$h= x^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! a^i$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\!: [ x = k ] \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{R}\\!: \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\not\\sim\\mathsf{R}\\qquad{}\\text{non-bisimilar}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\phi_L=[ \\tau ] (k = x)\\;,~~\\phi_R=\\langle{} \\tau \\rangle{} \\top{}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! a^i ,\\,\\sigma= [(k, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! a^i ,\\,\\sigma= [(k, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul>\n",
       "<ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! a^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "k = s2n \"k\"\n",
    "runBisimExperiment [All a,All k,All x]\n",
    "  ((x.=k)tau)\n",
    "  tau"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$h= a^i \\!\\!\\cdot\\! k^i$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\!: a ( x ).\\! [ x = k ] \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{R}\\!: a ( x ).\\! \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\not\\sim\\mathsf{R}\\qquad{}\\text{non-bisimilar}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\phi_L=\\langle{} a ( x )\\rangle{} [ \\tau ] (x = k)\\;,~~\\phi_R=[ a ( x )] \\langle{} \\tau \\rangle{} \\top{}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\phi_L=[ a ( x )] [ \\tau ] (x = k)\\;,~~\\phi_R=\\langle{} a ( x )\\rangle{} \\langle{} \\tau \\rangle{} \\top{}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= a^i \\!\\!\\cdot\\! k^i ,\\,\\sigma= [] \\quad {-} a (\\cdot){\\rightarrow{}}~~ ( x ).\\! [ x = k ] \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= a^i \\!\\!\\cdot\\! k^i ,\\,\\sigma= [] \\quad {-} a (\\cdot){\\rightarrow{}}~~ ( x ).\\! \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= a^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [(x, k)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= a^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [(x, k)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= a^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul>\n",
       "<ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= a^i \\!\\!\\cdot\\! k^i ,\\,\\sigma= [] \\quad {-} a (\\cdot){\\rightarrow{}}~~ ( x ).\\! \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= a^i \\!\\!\\cdot\\! k^i ,\\,\\sigma= [] \\quad {-} a (\\cdot){\\rightarrow{}}~~ ( x ).\\! [ x = k ] \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= a^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! x2^i ,\\,\\sigma= [(x2, k)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= a^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! x2^i ,\\,\\sigma= [(x2, k)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= a^i \\!\\!\\cdot\\! k^i \\!\\!\\cdot\\! x2^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "k = s2n \"k\"\n",
    "runBisimExperiment [All k,All a]\n",
    "  ( inp a$x.\\ ((x.=k)tau) )\n",
    "  ( inp a$x.\\ tau )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$h= k^i \\!\\!\\cdot\\! a^i$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\!: a ( x ).\\! [ x = k ] \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{R}\\!: a ( x ).\\! \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\not\\sim\\mathsf{R}\\qquad{}\\text{non-bisimilar}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\phi_L=\\langle{} a ( x )\\rangle{} [ \\tau ] (x = k)\\;,~~\\phi_R=[ a ( x )] \\langle{} \\tau \\rangle{} \\top{}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\phi_L=[ a ( x )] [ \\tau ] (x = k)\\;,~~\\phi_R=\\langle{} a ( x )\\rangle{} \\langle{} \\tau \\rangle{} \\top{}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= k^i \\!\\!\\cdot\\! a^i ,\\,\\sigma= [] \\quad {-} a (\\cdot){\\rightarrow{}}~~ ( x ).\\! [ x = k ] \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= k^i \\!\\!\\cdot\\! a^i ,\\,\\sigma= [] \\quad {-} a (\\cdot){\\rightarrow{}}~~ ( x ).\\! \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= k^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [(x, k)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= k^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [(x, k)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= k^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul>\n",
       "<ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= k^i \\!\\!\\cdot\\! a^i ,\\,\\sigma= [] \\quad {-} a (\\cdot){\\rightarrow{}}~~ ( x ).\\! \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= k^i \\!\\!\\cdot\\! a^i ,\\,\\sigma= [] \\quad {-} a (\\cdot){\\rightarrow{}}~~ ( x ).\\! [ x = k ] \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= k^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x2^i ,\\,\\sigma= [(x2, k)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= k^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x2^i ,\\,\\sigma= [(x2, k)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= k^i \\!\\!\\cdot\\! a^i \\!\\!\\cdot\\! x2^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "k = s2n \"k\"\n",
    "runBisimExperiment [All a, All k]\n",
    "  ( inp a$x.\\ ((x.=k)tau) )\n",
    "  ( inp a$x.\\ tau )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$h= x^i \\!\\!\\cdot\\! y^i$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\!: \\tau\\!.\\! [ x = y ] \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{R}\\!: \\tau\\!.\\! 0 + \\tau\\!.\\! \\tau\\!.\\! 0$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\mathsf{L}\\not\\sim\\mathsf{R}\\qquad{}\\text{non-bisimilar}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\phi_L=\\langle{} \\tau \\rangle{} ([ y = x ] \\langle{} \\tau \\rangle{} \\top{} \\land{} [ \\tau ] (y = x))\\;,~~\\phi_R=[ \\tau ] ([ \\tau ] \\bot{} \\lor{} \\langle{} \\tau \\rangle{} \\top{})$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\phi_L=[ \\tau ] [ y = x ] \\langle{} \\tau \\rangle{} \\top{}\\;,~~\\phi_R=\\langle{} \\tau \\rangle{} [ \\tau ] \\bot{}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style>$\\phi_L=[ \\tau ] [ \\tau ] (y = x)\\;,~~\\phi_R=\\langle{} \\tau \\rangle{} \\langle{} \\tau \\rangle{} \\top{}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ [ x = y ] \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [(y, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [(y, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [(y, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul>\n",
       "<ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ [ x = y ] \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [(y, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul>\n",
       "<ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ [ x = y ] \\tau\\!.\\! 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{blue}{\\mathsf{L}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [(y, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [(y, x)] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> <ul class='nested'> <li> <label> $\\color{red}{\\mathsf{R}\\!: h= x^i \\!\\!\\cdot\\! y^i ,\\,\\sigma= [] \\quad {-} \\tau {\\rightarrow{}}~~ 0 }$ </label> </li> </ul> </ul> </ul>\n"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "runBisimExperiment axay (taup $ (x.= y) tau) (tau .+ taup tau)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment axay (taup ((x.= y) tau) .+ t_tt) t_tt"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment axay (tau .+ taup tau) (taup $ (x.= y) tau)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment [All x] (inp x$z.\\tau .+ tau) (inp x$z.\\tau .+ out z x o)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment axayazaw ((z.= w) tau) ((x.= y) tau)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment axayaaab ppp1 qqq1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "{-# LANGUAGE PartialTypeSignatures #-}\n",
    "runFreshMT $ OpS.one (reverse [All a,Nab x,All y]) ((x.=y)tau) :: [(EqC,(Act,Pr))]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment [All a] ppp2 qqq2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment axay ((x.= y) (taup tau) .+ tau) (taup tau .+ tau)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment axay (taup ((x.= y) tau) .+ t_tt) t_tt"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment axay (tau .+ taup tau) (taup $ (x.= y) tau)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment [All x] (inp x$z.\\tau .+ tau) (inp x$z.\\tau .+ out z x o)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment axayazaw ((z.= w) tau) ((x.= y) tau)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment axayaaab ppp1 qqq1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment [All a] ppp2 qqq2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment axay ((x.= y) (taup tau) .+ tau) (taup tau .+ tau)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment axay (taup tau .+ tau) ((x.= y) (taup tau) .+ tau)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment [All a] (Nu$b.\\(inp a $x.\\(x.= b) (out x x o))) (Nu$b.\\(inp a $x.\\o))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "runBisimExperiment [All a] (Nu$b.\\out a b (inp a $x.\\(x.= b) (out x x o))) (Nu$b.\\out a b (inp a $x.\\out x x o))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "k = s2n \"k\"\n",
    "runBisimExperiment [All x, All k]\n",
    "  ( tau .+ taup tau .+ taup((x.=k)tau) )\n",
    "  ( tau .+ taup tau )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "k = s2n \"k\"\n",
    "runBisimExperiment [All a, All k]\n",
    "  ( inp a$x.\\ tau .+ taup tau .+ taup((x.=k)tau) )\n",
    "  ( inp a$x.\\ tau .+ taup tau )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "k = s2n \"k\"\n",
    "runBisimExperiment [All a]\n",
    "  ( Nu$k.\\out a k ( inp a$x.\\ tau .+ taup tau .+ taup((x.=k)tau) ) ) -- L\n",
    "  ( Nu$k.\\out a k ( inp a$x.\\ tau .+ taup tau                    ) ) -- R"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# some not so quick things TODO\n",
    "\n",
    " 1. refactoring to reduce code ducplications\n",
    " 1. manage inequality feature and other notions of bisimulation (early,quasiopen) seamlessy with a single codebase\n",
    "\n",
    "these should be useful (almost necessary) thing to do if we want to work on an algorithm\n",
    "that adapts from failure of open bisim to see whether quasi-open is acheivable from there.\n",
    "\n",
    "And, there are also explorations on how to suppport additional features/variants of pi-calculus: applied-pi style terms, replication, etc"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Haskell",
   "language": "haskell",
   "name": "haskell"
  },
  "language_info": {
   "codemirror_mode": "ihaskell",
   "file_extension": ".hs",
   "name": "haskell",
   "pygments_lexer": "Haskell",
   "version": "8.6.5"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}