-- proof of concept Haskell code to go with (used as demo in) the presentation
-- Proof by Picture?!
-- http://www.javakade.nl/research/talk/proofbypicture.pdf
-- for showing constructive confluence based on the technology from:
-- Critical Peaks Redefined Φ ⊔ Ψ = ⊤, IWC 2017
-- Confluence by Critical Pair Analysis Revisited, CADE 2019, DOI:10.1007/978-3-030-29436-6_19
-- by Hirokawa, N., Nagele, J., van Oostrom, V., Oyamaguchi, M.
-- based on the isomorphism between inductive and geometric multipatterns (Lemma 2 in CADE 2019)
--
-- main constructions are
-- 1) orthoDiamond: turns a multi-multi peak into multi-multi valley for orthogonal TRSs
-- 2) devclosedDiamond: turns a multi-one peak into a many-multi valley based on Okui's criterion
-- both by recursively decomposing peaks of multisteps into their critically overlapping parts, as per the papers
--
-- code partially finished in that
-- 1) comments refer to a preliminary version of CADE 2019
-- 2) functionality and experimentation for Okui only partial
-- 3) output to graphical format (dot) missing

-- Vincent van Oostrom, 2018-2026
-- Creative Commons Attribution 4.0 International License
-- https://creativecommons.org/licenses/by/4.0/

-- {-# LANGUAGE MultiParamTypeClasses #-}
-- {-# LANGUAGE TypeSynonymInstances #-}
-- {-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE FlexibleContexts #-}
-- {-# LANGUAGE FunctionalDependencies #-}
-- {-# LANGUAGE GeneralizedNewtypeDeriving #-}

import Data.Set (Set,singleton,union,intersection,unions,partition,fromList,null,toList,empty,isSubsetOf,findMin,delete,difference,filter,member) 
import qualified Data.Set as Set
import Data.List (nub)

-- page 2
-- Preliminaries
type Pfun a b = a -> Maybe b -- partial function
update :: (a->b) -> Pfun a b -> (a->b) -- update of (total) function with partial function
update f g x = case (g x) of
  Nothing ->  f x
  Just y -> y
  
-- page 3
-- Section 3.1
-- Definition 2
data SymbolType = TFunction | TVariable | TRule | TGap
class (Eq a,Ord a,Show a) => Signature a where
  arity :: a -> Int -- arity of a symbol
  stype :: a -> SymbolType -- symbol type
  genvar :: Int -> a -- genvar i, ith variable symbol, assumption is that variable indices are > 0
  gengap :: Int -> Int -> a -- gengap i n, ith gap symbol of arity n, again assume i > 0, n >= 0
  gapindex :: a -> Int -- index of gap (used for fresh gap generation), assumed > 0, 0 if other symbol
    -- could be done more abstractly by having a fresh-for-a-set-of-gap-symbols function
data Siga = Sym String Int | Var Int | Gap Int Int | Rule String Int -- a signature
  deriving (Eq,Ord)
symprd = Sym "p" 1 -- some ad hoc symbols
symsuc = Sym "s" 1
symzer = Sym "0" 0
asymzer = Sym "a" 0
bsymzer = Sym "b" 0
csymzer = Sym "c" 0
dsymzer = Sym "d" 0
asymbin = Sym "f" 2
arulzer = Rule "\960" 0
arulone = Rule "\960" 1
arultwo = Rule "\960" 2
arulthr = Rule "\960" 3
brulzer = Rule "\961" 0
brulone = Rule "\961" 1
brultwo = Rule "\961" 2
brulthr = Rule "\961" 3
crulzer = Rule "\962" 0
crulone = Rule "\962" 1
crultwo = Rule "\962" 2
crulthr = Rule "\962" 3
drulzer = Rule "\952" 0
drulone = Rule "\952" 1
drultwo = Rule "\952" 2
drulthr = Rule "\952" 3
asymGap = Gap 1 1
bsymGap = Gap 2 1
csymGap = Gap 2 0
dsymGap = Gap 3 2
esymGap = Gap 4 2
fsymGap = Gap 3 1
symGap13 = Gap 1 3
symGap12 = Gap 1 2
showGapIndex :: Int -> String
showGapIndex i = case i of
  1 -> "X"
  2 -> "Y"
  3 -> "Z"
  4 -> "U"
  5 -> "V"
  6 -> "W"
  i -> "G"++(show (i-6))
instance Show Siga where -- ad hoc pretty printing of symbols
  show (Sym s _) = s
  show (Var i) = "v"++(show i)
-- would be nice to use subscripts, but unicodes \0208x hex, i.e. 4224+x don't work on my terminal
  show (Gap i a) = (showGapIndex i)++(if (a == 1) then "" else ("/"++(show a)))
  show (Rule s _) = "\27[31m"++s++"\27[30m"
instance Signature Siga where
  genvar = Var
  arity (Sym _ ar) = ar
  arity (Var _) = 0
  arity (Gap _ ar) = ar
  arity (Rule _ ar) =ar
  stype (Sym _ _) = TFunction
  stype (Var _) = TVariable
  stype (Rule _ _) = TRule
  stype (Gap _ _) = TGap
  gengap = Gap
  gapindex (Gap i _) = i
  gapindex _ = 0
data Trm a = Fun {  -- terms without arity restriction; aka  as rose trees in fp; naive
  trmHead :: a,
  trmArgs :: [Trm a]
} deriving (Eq,Ord)
vara i = Fun (genvar i) [] :: Signature a => Trm a -- construct the ith variable, as term 
symprda = Fun symprd -- ad hoc symbol applications
symsuca = Fun symsuc
symzera = Fun symzer []
symzeraa = Fun asymzer []
symzerba = Fun bsymzer []
symzerca = Fun csymzer []
symzerda = Fun dsymzer []
symbina = Fun asymbin
symGapa = Fun asymGap
symGapb = Fun bsymGap
symGapc = Fun csymGap []
symGapd = Fun dsymGap
symGape = Fun esymGap
symGapf = Fun fsymGap
symGap13a = Fun symGap13
symGap12a = Fun symGap12
rulzera = Fun arulzer []
rulzerb = Fun brulzer []
rulzerc = Fun crulzer []
rulzerd = Fun drulzer []
rulonea = Fun arulone
rultwoa = Fun arultwo
rulthra = Fun arulthr
ruloneb = Fun brulone
rultwob = Fun brultwo
rulthrb = Fun brulthr
rulonec = Fun crulone
rultwoc = Fun crultwo
rulthrc = Fun crulthr
ruloned = Fun drulone
rultwod = Fun drultwo
rulthrd = Fun drulthr

showListAsTuple :: Show a => [a] -> String
showListAsTuple [] = ""
showListAsTuple [t] = "("++(show t)++")"
showListAsTuple (t:ts) = "("++(show t)++(foldr (\x->((++) (","++(show x)))) ")" ts)
instance (Show a) => Show (Trm a) where -- show terms in usual prefix notation with parentheses
  show (Fun h ts) = (show h)++(showListAsTuple ts)
isTrm :: Signature a => Trm a -> Bool -- check whether term is term over signature
isTrm (Fun s ts) = (arity s == length ts) && (all isTrm ts) 
-- isTrm (symsuca[symprda[]]) is False, p(s()), but isTrm (symsuca[symprda[symzera]]) is True,p(s(0))
type Trma = Trm Siga -- terms over a signature
type Alg a b = a -> [b] -> b -- algebra
type Alga b = Alg Siga b -- algebra for a fixed signature
alg :: Alg a b -> Trm a -> b -- algebra evaluation
alg f (Fun sym ts) = f sym (fmap (alg f) ts)
alga = alg :: Alga b -> Trma -> b -- specialisation to a signature
type AlgTrm a = Alg a (Trm a) -- type of term algebra over signature a 
algTrm = Fun :: AlgTrm a -- term algebra
-- alg algTrm t is t for all t, e,g, alg algTrm (symsuca[symprda[symzera]]) is s(p(0))

-- in-text definitions and observations
pfunEmp :: Pfun a b -- totally undefined function
pfunEmp _ = Nothing
pfunPair :: Eq a => Pfun a b -> (a,b) -> Pfun a b -- update partial function with single input-output pair
pfunPair f (x,y) z = if (x == z) then Just y else f z
type PfunGraph a b = [(a,b)] -- partial function given by function graph, input-output pairs
-- consider using data type to be able to show as pair of lists instead of list of pairs
graphPfun :: Eq a => PfunGraph a b -> Pfun a b -- convert function graph to partial function
graphPfun = foldl pfunPair pfunEmp 
updateGraph :: Eq a => (a->b) -> PfunGraph a b -> (a -> b)
updateGraph f g = update f (graphPfun g) -- update function f by graph of function g
-- (updateGraph id [(3,4)]) 3 is 4, but (updateGraph id [(3,4)]) x is x for x not 3
-- later pairs `overwrite' previous ones
-- (updateGraph id [(3,4),(3,5)]) 3
unitLift :: a -> [a] -> a -- lifts value b to function unit -> b 
unitLift x [] = x -- should only be applied to empty list (2nd arg), error otherwise
varnGraph :: Signature a => [b] -> PfunGraph a ([b]->b) -- (gives rise to need for genvar in signature)
varnGraph l = zip (map genvar [1..]) (map unitLift l) -- make graph [v1:=b1,...,vn:=bn] out of [b1,...,bn]
updateVarn :: Signature a => Alg a b -> [b] -> Alg a b
updateVarn f l = updateGraph f (varnGraph l) -- update algebra f on initial vars [v1,...,vn] with values [b1,...,bn]

-- Example 3
algUnion :: Ord a => Alg a (Set a) -- symbols algebra, union of arguments
algUnion sym ss = unions ss
algSym :: Ord a => Alg a (Set a) -- symbols algebra, head symbol and union of arguments
algSym sym ss = union (singleton sym) (algUnion sym ss)
algSymVar :: Signature a => Pfun a ([Set a] -> Set a) -- update to map variables to symbols
algSymVar s = case (stype s) of
  TVariable -> Just (algSym s)
  _ -> Nothing
algVar :: Signature a => Alg a (Set a) -- variables algebra
algVar = update algUnion algSymVar 
trma = symprda [symsuca [symprda [symsuca [symzera]]]] :: Trma -- p(s(p(s(0))))
trmb = symsuca [symprda [vara 1]] :: Trma -- s(p(v1))
-- alg algSym trma = fromList [p,s,0], alg algVar trma = fromList []
-- alg algSym trmb = fromList [p,s,v1], alg algVar trmb = fromList [v1]

-- algebras not in text
algSum :: Alg a Int -- sum algebra, sum of arguments
algSum sym ns = sum ns
algSize :: Alg a Int -- size algebra, head symbol plus sum of arguments
algSize sym ns = 1+(algSum sym ns)
algSizeVar :: Signature a => Pfun a ([Int] -> Int) -- update to map var1iables to 0
algSizeVar s = case (stype s) of
  TVariable -> Just (algSum s)
  _ -> Nothing
algPSize :: Signature a => Alg a Int
algPSize = update algSize algSizeVar -- psize algebra (discarding variables)
-- alg algSize trma = 5, alg algSize trmb = 3, algPsize trmb = 2

-- Example 4
type Pos = [Int] -- positions (should really be positive nats instead of ints)
posEmp = [] :: Pos -- empty position 
posn n = [n] :: Pos
posSco = (++) :: Pos -> Pos -> Pos -- sequential composition
data PosTyp = Edg | Vtx -- types of positions, vertex and edge
  deriving (Eq,Ord)
instance Show PosTyp where
   show Edg = "\0773" -- macron accent on previous char
   show Vtx = "\0778" -- ring accent on previous char
data TPos = TPos Pos PosTyp -- vertex/edge positions
  deriving (Eq,Ord) -- per construction  the derived order on positions is the left-outer order
showListAsSeq :: Show a => [a] -> String
showListAsSeq [] = "\0949" -- epsilon for empty string
showListAsSeq [t] = show t
showListAsSeq (t:ts) = (show t)++(foldr (\x->((++) ("."++(show x)))) "" ts)
instance Show TPos where
  show (TPos p t) = (showListAsSeq p) ++ (show t)
vtxTPosEmp = TPos posEmp Vtx :: TPos
edgTPosEmp = TPos posEmp Edg :: TPos
vtxTPosn n = TPos (posn n) Vtx :: TPos
edgTPosn n = TPos (posn n) Edg :: TPos
posTSco :: TPos -> TPos -> TPos -- typed sequential composition, type is that of snd 
posTSco (TPos p t) (TPos q s) = TPos (posSco p q) s
-- for vector/matrices we do something ad hoc (Data.Matrix requires Num which requires way too much, is ugly)
type SetTPos = Set TPos -- sets of typed positions
stposSum = union :: SetTPos -> SetTPos -> SetTPos -- addition
stposZer = empty :: SetTPos -- two-sided unit for addition
stposMul :: SetTPos -> SetTPos -> SetTPos
stposMul s t = fromList [posTSco x y| x <- (toList s),y<- (toList t)] -- multiplication
stposLone = singleton vtxTPosEmp :: SetTPos -- left unit for multiplication
type VecSetTPos = [SetTPos] -- column vector, only used for dimension 2
dotmul ::  VecSetTPos ->  VecSetTPos -> SetTPos
dotmul u v = foldl stposSum stposZer (zipWith stposMul u v)
vecSTPosZer = [stposZer,stposZer] :: VecSetTPos -- empty positions vector
vecSTPosn n = [stposZer,singleton (vtxTPosn n)] :: VecSetTPos -- (0,{n}) vector
vecSTPosnn n = [singleton (vtxTPosn n),singleton (vtxTPosn n)] :: VecSetTPos -- ({n},{n}) vector
vecSTPosOne = [singleton edgTPosEmp,singleton vtxTPosEmp] :: VecSetTPos -- root position vector
type MatrixSetTPos = [VecSetTPos] -- matrix, only used for dimension 2
matrixSTPosn n = [vecSTPosZer,vecSTPosn n] :: MatrixSetTPos -- ((0,0),(0,{n})) matrix
matrixSTPosnn n  = [vecSTPosZer,vecSTPosnn n] :: MatrixSetTPos -- ((0,0),({n},{n})) matrix
matrixvecmul ::  MatrixSetTPos -> VecSetTPos ->  VecSetTPos
matrixvecmul m v = [dotmul u v| u <- m]
matrixvecmuln :: Int -> VecSetTPos -> VecSetTPos
matrixvecmuln n = matrixvecmul (matrixSTPosn n)
matrixvecmulnn :: Int -> VecSetTPos -> VecSetTPos
matrixvecmulnn n = matrixvecmul (matrixSTPosnn n)
vecsum = zipWith stposSum :: VecSetTPos ->  VecSetTPos ->  VecSetTPos -- sum of two vectors
algShift :: Alg a VecSetTPos -- shift algebra, shifting arguments
algShift sym ps = foldl vecsum vecSTPosZer (zipWith matrixvecmuln [1..] ps)
algTree :: Alg a VecSetTPos -- tree algebra, adjoining root to and keeping internal edges
algTree sym ps = foldl vecsum vecSTPosOne (zipWith matrixvecmulnn [1..] ps)
algTreeVar :: Signature a => Pfun a ([VecSetTPos] -> VecSetTPos) -- update to map variables to empty vectors
algTreeVar s = case (stype s) of
  TVariable -> Just (algShift s)
  _ -> Nothing
algPTree :: Signature a => Alg a VecSetTPos
algPTree = update algTree algTreeVar -- ptree algebra (discarding variables)
-- type should be generalised to arbitrary signature for proper Signature class
external ::  VecSetTPos -> SetTPos
external [s,_] = s -- empty or singleton external position; should always be edge position
-- page 4
internal ::  VecSetTPos -> SetTPos
internal [_,t] = t -- set of internal positions
trmc = symprda [symsuca [symprda [symsuca [vara 1]]]] :: Trma -- p(s(p(s(v1))))
-- alg algPTree trmc = [fromList [ε̅],fromList [ε̊,1̅,1̊,1.1̅,1.1̊,1.1.1̅,1.1.1̊]]
-- internal (alg algPTree trmc) = fromList [ε̊,1̅,1̊,1.1̅,1.1̊,1.1.1̅,1.1.1̊]
-- output looks garbled in emacs, but is ok in the terminal and the textedit app

-- Lemma 5, second item
algTrmList = updateVarn algTrm  :: [Trma] -> Alga Trma -- substitution for initial vars
trmd = alga (algTrmList [trmb]) trmc -- p(s(p(s(v1))))[v1:= s(p(v1))] = p(s(p(s(s(p(v1))))))
-- resulting term has same size as trmc with v1 updated to the size of trmb:
-- alga algSize trmd = 7 = alg (updateVarn algSize (map (alga algSize) [trmb])) trmc 

-- Definition 6
trmAlgn :: Signature a => Trm a -> Alg a b -> Int -> [b] -> b
  -- turn term into n-ary function by updating v1,...,vn with value b1,...,bn
  -- requires symbols to have an arity
  -- dependency between length l and n checked by having only 1 case
trmAlgn t a n l = case (n == length l) of
  True -> alg (updateVarn a l) t
-- trmAlgn fails if arity is not ok
type Assignment a = a -> (Trm a) -- total assignment, function from signature to terms
type Assignmenta = Assignment Siga
type PfunGraphTrm a = PfunGraph a (Trm a) -- assignment graph, list of signature,term pairs 
type PfunGraphTrma = PfunGraphTrm Siga
type PAssignment a = Pfun a (Trm a) -- partial assignment, partial function from signature to terms
type PAssignmenta = PAssignment Siga
assAlgTrm :: Signature a => Assignment a -> AlgTrm a -- substitution algebra associated to (total) assignment
assAlgTrm s f = trmAlgn (s f) algTrm (arity f)
gassGraphTrm :: Signature a => PfunGraphTrm a -> PfunGraph a ([Trm a]->Trm a) -- substitution graph for assignment graph
gassGraphTrm = map (\x->(fst x,trmAlgn (snd x) algTrm (arity (fst x)))) 
passPfunTrm :: Signature a => PAssignment a -> Pfun a ([Trm a]->Trm a) -- partial substitution for partial assignment
passPfunTrm s f = case (s f) of
  Nothing -> Nothing
  Just t -> Just (trmAlgn t algTrm (arity f))
trmAss :: Signature a => Assignment a -- term assignment, mapping n-ary f to the term f(v1,...,vn)
trmAss s = Fun s (map vara [1..(arity s)])
trmSubst :: Signature a => AlgTrm a  -- term substitution for Siga
trmSubst = assAlgTrm trmAss

-- in text definition and observations
-- alg algSize trmd = 7 = trmAlgn trmd algSize 0 []
-- e.g. alg trmSubst trmd is p(s(p(s(s(p(v1)))))) is trmd

-- Remark
assa = [(asymGap,trmb)] :: PfunGraphTrma -- example tree homomorphism [X:=s(p(v1))]
-- alg (assAlgTrm (updateGraph trmAss assa)) trmd = trmd, no effect since X does not occur
assb = [(symprd,trmb)] :: PfunGraphTrma -- example tree homomorphism [p:=s(p(v1))]
-- alg (assAlgTrm (updateGraph trmAss assb)) trmd = s(p(s(s(p(s(s(s(p(v1)))))))))
assc = [(symsuc,trma)]  :: PfunGraphTrma -- example tree homomorphism [p:=p(s(p(s(0))))]
-- alg (assAlgtrm (updateGraph trmAss assc)) trmd = p(p(s(p(s(0))))), because of erasure

-- Example 7
trme = symprda [symsuca [vara 1]] :: Trma -- term p(s(v1))
assd = [(asymGap,trme)] :: PfunGraphTrma -- example partial assignment [X:=p(s(v1))]
trmf = symprda [symsuca [symGapa [symzera]]] :: Trma -- term p(s(X(0)))
-- alg (assAlgTrm (updateGraph trmAss assd)) trmf = p(s(X(0))[[X:=s(p(v1))]] = p(s(p(s(0))))
asse = [(asymGap,trmc)] -- partial assignment [X:=p(s(p(s(v1)))]
-- asse^Tree is used before it is defined in Definition 8, so see below.

-- Definition 8
assAlg :: Signature a => Alg a b -> Assignment a -> Alg a b
assAlg f x s = trmAlgn (x s) f (arity s) -- transform assignment into algebra, by interpreting its terms
passPfun :: Signature a => Alg a b -> PAssignment a -> Pfun a ([b]->b) -- partial assignments into partial algebra
passPfun f x s = case (x s) of
  Nothing -> Nothing
  Just t -> Just (trmAlgn t f (arity s))
gassGraph :: Signature a => Alg a b -> PfunGraphTrm a -> PfunGraph a ([b]->b) -- graph assignment into graph algebra
gassGraph f = map (\x->(fst x,trmAlgn (snd x) f (arity (fst x))))
assSco :: Signature a => Assignment a -> Assignment a -> Assignment a -- sequential composition of assignments
assSco f g s = alg (assAlgTrm g) (f s)
passSco :: Signature a => PAssignment a -> PAssignment a -> PAssignment a -- idem for partial assignment
passSco f g s = case (f s) of
  Nothing -> Nothing
  Just t -> Just (alg (update algTrm (passPfunTrm g)) t)
gassSco :: Signature a => PfunGraphTrm a -> PfunGraphTrm a -> PfunGraphTrm a -- idem for graph assignment
gassSco f g = map (\x->(fst x,alg (updateGraph algTrm (gassGraphTrm g)) (snd x))) f
idVar :: Signature a => a -> Trm a -> Bool  -- test, if symbol is a variable, the term is that variable
idVar s t = case (stype s) of
  TVariable -> s == trmHead t
  _ -> True
arityVars :: Signature a => a -> Trm a -> Bool -- test whether variables in term have indices <= arity of symbol
arityVars s t = isSubsetOf (alg algVar t) (fromList (map genvar [1..(arity s)]))

gassClosed :: Signature a => PfunGraphTrm a -> Bool -- check for closedness of graph assignment
gassClosed = all (\(s,t)-> (idVar s t) && (arityVars s t))

-- Example 7 continued
-- asse = [(asymGap,trmc)] -- partial assignment [X:=p(s(p(s(v1)))]
-- alg (updateGraph algTree (gassGraph algTree asse)) (symGapa[symzera]), results in
-- [fromList [ε̅],fromList [ε̊,1̅,1̊,1.1̅,1.1̊,1.1.1̅,1.1.1̊,1.1.1.1̅,1.1.1.1̊]]
-- first (constant) component by applying it to X and the empty vector
--  (updateGraph algTree (gassGraph algTree asse)) asymGap [vecSTPosZer]
-- [fromList [ε̅],fromList [ε̊,1̅,1̊,1.1̅,1.1̊,1.1.1̅,1.1.1̊]]

-- page 5
-- Remark
trmg = symGapa[symzeraa] :: Trma -- X(a) = t
assg = [(asymGap,vara 1)] :: PfunGraphTrma -- [X:=v1] = sigma
assh = [(genvar 1,vara 2)] :: PfunGraphTrma -- [v1:=v2] = tau
-- first example
-- gassClosed assg = True, but gassClosed assh = False, 
-- alg (assAlgTrm (updateGraph trmAss assh)) (alg (assAlgTrm (updateGraph trmAss assg)) trmg) = a = (t^sigma)^tau, same
-- alg (updateGraph algTrm  (gassGraph (updateGraph algTrm (gassGraphTrm assh)) assg)) trmg = a = t^(sigma^tau)
-- but different from t^(tau o sigma), which is 
-- alg (assAlgTrm (updateGraph trmAss (gassSco assg assh))) trmg = v2
-- note that we update the term assignment here with the given composed assignment, and convert the result to an algebra
-- equivalently we can convert the composed assignment to a partial algebra first, and then update the term algebra
-- alg (updateGraph algTrm (gassGraphTrm (gassSco assg assh))) trmg = v2
-- second example
assi = [(asymGap,symGapc)] :: PfunGraphTrma -- [X:=Y] = sigma
assj = [(csymGap,vara 1)] :: PfunGraphTrma -- [Y:=v1] = tau
-- gassClosed assi = True, but gassClosed assj = False, again
-- alg (assAlgTrm (updateGraph trmAss assj)) (alg (assAlgTrm (updateGraph trmAss assi)) trmg) = v1 = (t^sigma)^tau, same
--  alg (updateGraph algTrm  (gassGraph (updateGraph algTrm (gassGraphTrm assj)) assi)) trmg =  v1 =  t^(sigma^tau)
-- but different from t^(tau o sigma), which is 
-- alg (assAlgTrm (updateGraph trmAss (gassSco assi assj))) trmg = a

-- Lemma 9
-- first item
-- example illustrating (t^sigma)^A = t^(sigma^A) for t =  p(s(X(0))), sigma = [X:=p(s(v1))], A = size
-- alg algSize (alg (updateGraph algTrm (gassGraphTrm assd)) trmf) =  (t^sigma)^A = 5 (size of p(s(p(s(0)))))
-- alg (updateGraph algSize (gassGraph algSize assd)) trmf  = 5 = t^(sigma^A)

-- Section 3.2

-- Definition 10
tposEnds :: TPos -> Set TPos -- set of vertices incident to a typed position (so only non-empty for edges)
tposEnds (TPos _ Vtx) = empty
tposEnds (TPos [] Edg) = singleton (TPos [] Vtx)
tposEnds (TPos p Edg) =  union (singleton (TPos (init p) Vtx)) (singleton (TPos p Vtx))
downwardClosed :: Ord a => (a -> Set a) -> (Set a) -> Bool -- downward closed of set wrt set-of-down elts
downwardClosed p s = (all (\x-> isSubsetOf (p x) s) (toList s))
posDownwardClosed :: Set TPos -> Bool -- downward closed wrt set-of-incidence, and no root edge
posDownwardClosed s = (downwardClosed tposEnds s) && (not (isSubsetOf (singleton (TPos [] Edg)) s))
data GeoCluster a = GeoCluster { -- geometric clusters as pairs of a term and subset of the internal positions
  clstrm :: Trm a, -- term of the cluster
  clspos :: Set TPos -- subset of the internal positions of the term
  } deriving (Eq,Ord)
instance Show a => Show (GeoCluster a) where
  show (GeoCluster t p) = "( "++(show t)++" | "++(show p)++" )"
type GeoClustera = GeoCluster Siga
isGeoCluster :: Signature a => GeoCluster a -> Bool -- set of positions is geometric cluster for term?
isGeoCluster (GeoCluster t s) = (posDownwardClosed s) && (isSubsetOf s (internal (alg algPTree t)))

tposPrd :: TPos -> TPos -- predecessor function on positions, in tree. predecessor is a prefix
tposPrd (TPos p Vtx) = (TPos p Edg) -- on a vertex it's an edge
tposPrd (TPos [] Edg) = (TPos [] Edg) -- identity on root edge
tposPrd (TPos p Edg) = (TPos (init p) Vtx) -- an a (non-root) edge it's a vertex
addTPos :: (Set TPos) -> (TPos -> TPos) -> TPos -> (TPos -> TPos) -- update representative function
addTPos s f x y = if ((x == y) && (isSubsetOf (singleton (tposPrd x)) s)) then (f (tposPrd x)) else (f y)
repTPos :: (Set TPos) -> (TPos -> TPos) -- represent connected component, i.e. pattern, by mapping to its root position
  -- iteration uses that the prefixes of a position are processed before the position itself
repTPos s = foldl (addTPos s) id (toList s)
isGeoPattern :: Signature a => Set TPos -> Trm a -> Bool -- set of positions is geometric pattern for term?
isGeoPattern s t = case (toList s) of
  [] -> False
  (p:ps) -> (isGeoCluster (GeoCluster t s)) && (let rep = repTPos s in (all (\q -> rep p == rep q) ps))
data GeoPatternCluster a = GeoPatternCluster {
  pattrm :: Trm a, -- term of the cluster
  clsposs :: Set (Set TPos) -- set of (non-overlapping) subsets of the internal positions of the term
}
type GeoPatternClustera = GeoPatternCluster Siga
isPartition :: Ord a => [Set a] -> Bool -- test whether sets in list are pairwise disjoint
isPartition [] = True
isPartition (s:ss) = all (\t->Set.null (intersection s t)) ss
isGeoPatternCluster :: Signature a => GeoPatternCluster a -> Bool
isGeoPatternCluster (GeoPatternCluster t ss) = (isPartition l) && (all (\p -> isGeoPattern p t) l)
  where l = toList ss                                                                            

-- in running text
gclsLe = isSubsetOf :: Set TPos -> Set TPos -> Bool -- geometric refinement order
-- assumes both sets are subsets of the internal positions of the same term
-- lattice operations, doesn't check for these being clusters (or for the same term)
gclsBot = empty :: Set TPos
gclsLub = union :: Set TPos -> Set TPos -> Set TPos
gclsGlb = intersection :: Set TPos -> Set TPos -> Set TPos
gclsTop :: Signature a => Trm a -> Set TPos
gclsTop t = internal (alg algPTree t)
data GeoWitness a = GeoWitness {
  patlft :: Set TPos,
  geotrm :: Trm a,
  patrgt :: Set TPos
  } deriving (Eq,Ord)
instance Show a => Show (GeoWitness a) where
  show (GeoWitness l t r) = (show l)++" \8838"++(show t)++" "++(show r)
type GeoWitnessa = GeoWitness Siga
isGeoWitness :: Signature a => GeoWitness a -> Bool
isGeoWitness (GeoWitness l t r) = (isGeoCluster (GeoCluster t l)) && (gclsLe l r) && (isGeoCluster (GeoCluster t r))

-- Lemma 11
gclsaux :: (TPos -> TPos) -> Set TPos -> Set (Set TPos)
gclsaux f s = if (Set.null s) then empty else let x = findMin s in let (p,t) = partition (\y -> f x==f y) s in (union (singleton p) (gclsaux f t))
gclsPartition :: Set TPos -> Set (Set TPos) -- partition a cluster into patterns
gclsPartition s = gclsaux (repTPos s) s 
one :: (a -> Bool) -> [a] -> Bool -- exists unique (cf. all and any)
one p [] = False
one p (x:xs) = if (p x) then (not (any p xs)) else (one p xs)
funaux :: (a->a->Bool) -> [a] -> a -> Bool
funaux r k x = one (r x) k
funLift :: (a->a->Bool) -> [a] -> [a] -> Bool -- forall-exists unique extension of relation
funLift r l k = all (funaux r k) l 
-- for some reason typechecking failed with inlined funaux ?
-- funLift (<) [3,4] [5] is True, funLift (<) [3,4] [5,6] is False
-- funLift (<) [5] [5,6] is True, funLift (<) [5,6] [5,6] is False
gclsPLe ::  Set (Set TPos) ->  Set (Set TPos) -> Bool
gclsPLe s t = funLift isSubsetOf (toList s) (toList t)

-- Example 12
poslista = [(TPos [] Vtx),(TPos [1,1] Vtx),(TPos [1,1,1] Edg),(TPos [1,1,1] Vtx)] :: [TPos]
posseta = fromList poslista :: Set TPos
-- isGeoCluster posseta trmc is True, isGeoPattern posseta trmc is False
-- isGeoCluster posseta trmb is False, isGeoPattern (fromList [(TPos [] Edg),(TPos [] Vtx)]) trmb is False
-- gclsPartition posseta is fromList [fromList [ε̊],fromList [1.1̊,1.1.1̅,1.1.1̊]]
poslistb = [(TPos [] Vtx),(TPos [1,1] Vtx),(TPos [1,1,1] Vtx)] :: [TPos]
possetb = fromList poslistb :: Set TPos
-- isGeoCluster possetb trmc is True, isGeoPattern possetb trmc is False
-- gclsPartition possetb is fromList [fromList [ε̊],fromList [1.1̊],fromList [1.1.1̊]]
-- gclsLe posseta possetb is False, gclsLe possetb posseta is True,
-- gclsLe posseta posseta is True
-- gclsPLe (gclsPartition posseta) (gclsPartition possetb) is False,
-- gclsPLe (gclsPartition possetb) (gclsPartition posseta) is True
-- gclsPLe (gclsPartition posseta) (gclsPartition posseta) is True
-- in accordance with the 1st item of Lemma 11
-- all (\x -> isGeoPattern x trmc) (toList (gclsPartition posseta)) is True, partitioned into patterns
poslistc = [(TPos [1,1,1] Edg)] :: [TPos]
possetc = fromList poslistc :: Set TPos
-- isGeoCluster (GeoCluster  trmc possetc) is False (end-vertex missing)
poslistd = [(TPos [1,1,1,1] Vtx)] :: [TPos]
possetd = fromList poslistd :: Set TPos
-- isGeoCluster (GeoCluster trmc  possetd) is False (variable position)

-- page 6
-- Definition 13
data InduCluster a = InduCluster { -- Inductive Cluster
  skeleton :: Trm a,     -- skelton term 
  gapass :: PfunGraphTrm a -- assignment, should be closed assignment for gaps
} deriving (Ord,Eq)
instance Show a => Show (InduCluster a) where
  show (InduCluster s g) = "( "++(show s)++" | "++(show g)++" )"
induClusterFor :: Signature a => InduCluster a -> Trm a -- term the cluster is for
induClusterFor c = alg (updateGraph algTrm (gassGraphTrm (gapass c))) (skeleton c)
isGap :: Signature a => a -> Bool -- test whether symbol is a gap (could be put in Signature interface maybe?)
isGap s = case (stype s) of
  TGap -> True
  _ -> False
isVar :: Signature a => a -> Bool -- test whether symbol is a var
isVar s = case (stype s) of
   TVariable -> True
   _ -> False
graphDomain = map fst :: PfunGraph a b -> [a] -- domain of partial function represented as graph
graphRange = map snd :: PfunGraph a b -> [b] -- range of partial function represented as graph
isLinearList :: Eq a => [a] -> Bool -- test whether list is without repetition
isLinearList l = (l == nub l) -- by testing whether it is the  same as after removing duplicates
-- assumes nub preserves order; can be more efficiently implemented in case Ord a
graphIsPfun :: Eq a => PfunGraph  a b -> Bool -- check whether graph is partial function
graphIsPfun = isLinearList . graphDomain -- i.e. whether domain is linear 
algSymList :: Ord a => Alg a [a] -- symbol list  algebra, head symbol and concat of arguments
algSymList sym ss = sym:(concat ss)
symList :: Ord a => Trm a -> [a]
symList = alg algSymList -- symbol list of a term, in preorder
gapsList :: Signature a => Trm a -> [a] -- list of gap symbol occurring in a term (i.e. may contain duplicates)
gapsList t = Prelude.filter isGap (symList t)
varsList :: Signature a => Trm a -> [a] -- list of var symbol occurring in a term (i.e. may contain duplicates)
varsList t = Prelude.filter isVar (symList t) 
isInduCluster :: Signature a => InduCluster a -> Bool -- check conditions on assignment, partial function and closed for gaps
isInduCluster c = let g = gapass c in (gassClosed g) &&  (all (\x->isGap (fst x)) g)
  && (graphIsPfun g)
  -- && (isSubsetOf (fromList (gapsList (skeleton c))) (fromList (graphDomain g)))
  -- this condition, that all gaps are assigned to,  not in paper so
  -- omitted for now; gives more freedom during abstraction from patterns
isLinearInduCluster :: Signature a => InduCluster a -> Bool -- check for linearity of cluster
isLinearInduCluster c = case (graphDomain (gapass c)) of
  d@[s] -> d == (Prelude.filter ((==) s) (gapsList (skeleton c)))
  _ -> False
nvars :: Signature a => Int -> [a] -- initial segment of length n of the variables
nvars n = map genvar [1..n]
-- for example nvars 4::[Siga] is [v1,v2,v3,v4] ;
isStandard :: Signature a => Trm a -> Bool -- check whether variables are named in standard way in a term
isStandard t = l == (nvars (length l)) where l = nub (varsList t)
  -- according to metivier, i.e. for each v_i+1 there is v_i to its left
  -- isStandard (symbina[vara 1,vara 1]) is True
  -- isStandard (symbina[vara 2,vara 1]) is False
  -- isStandard (symbina[vara 1,symbina[vara 2,vara 1]]) is True
  -- isStandard (symbina[vara 1,symbina[vara 1,vara 2]]) is True
headTrm :: Trm a -> a -- head of a term
headTrm (Fun s _) = s
isPatternSkeleton :: Signature a => Trm a -> Bool -- check pattern conditions on skeleton
isPatternSkeleton t = isLinearList (gapsList t) && (not (isVar (headTrm t)))
isPatternGapass :: Signature a => PfunGraphTrm a -> Bool -- check pattern conditions on graph assignment
isPatternGapass =  all (\(s,p)->(isStandard p) && ((nvars (arity s)) == varsList p)) 
isPatternInduCluster :: Signature a => InduCluster a -> Bool -- check for patternness of cluster
isPatternInduCluster c = isPatternSkeleton (skeleton c) && isPatternGapass (gapass c)
data InduWitness a = InduWitness -- witnesses to the refinement order on pattern clusters
  { clslft  :: InduCluster a,
    witness :: PfunGraphTrm a,
    clsrgt :: InduCluster a } deriving (Eq,Ord)
instance Show a => Show (InduWitness a) where
  show (InduWitness l w r) = (show l)++" \8849"++(show w)++" "++(show r)
type InduWitnessa = InduWitness Siga
isInduWitness :: Signature a => InduWitness a -> Bool -- check whether witness is indeed witnessing refinement
isInduWitness (InduWitness l w r) = (isInduCluster l) && (isPatternInduCluster l)
  && (graphIsPfun w) && (gassClosed w)  && (isPatternGapass w)
  && (isInduCluster l) && (isPatternInduCluster r) &&
  induClusterFor l == induClusterFor r &&
  t == alg (updateGraph algTrm (gassGraphTrm w)) s &&
  h == gassSco w g
  where t = skeleton l
        g = gapass l
        s = skeleton r
        h = gapass r
data CAlg a b = CAlg { -- cluster algebra
  alglft :: (Alg a b),
  embed  :: (b->b),
  algrgt :: (Alg a b)}
calg :: Signature a => CAlg a b -> InduCluster a -> b -- cluster algebra interpretation
calg (CAlg l e r) (InduCluster t g) =
    alg (updateGraph l (map (\(s,u) -> (s,e.(trmAlgn u r (arity s)))) g)) t
algCAlg :: Alg a b -> CAlg a b -- embed algebras into cluster algebras
algCAlg f = CAlg f id f
algCAlgTrm :: CAlg a (Trm a) -- embed term algebra
algCAlgTrm = algCAlg algTrm

-- Example 14
trmh = symGapa[symsuca[symGapb[vara 1]]] :: Trma
assk = [(asymGap,symprda[vara 1]),(bsymGap,symprda[symsuca[vara 1]])] :: PfunGraphTrma
clsa = InduCluster trmh assk :: InduCluster Siga
-- isInduCluster clsa is True
-- isInduCluster (InduCluster trmh [(asymGap,symprda[vara 1])]) is False
-- induClusterFor clsa is p(s(p(s(v1))))
-- alg algSymList trmh is [X,s,Y,v1]
-- gapsList trmh is [X,Y]
-- isLinearInduCluster clsa is False
-- isPatternInduCluster clsa is True
clsb = InduCluster (symGapa[symGapa[vara 1]]) [(asymGap,symprda[vara 1])] :: InduCluster Siga
-- isInduCluster clsb is True, but isLinearInduCluster clsb is False
-- isLinearInduCluster (InduCluster (symGapa[vara 1]) [(asymGap,symprda[vara 1])]) is True
-- isLinearInduCluster (InduCluster (symGapa[vara 1]) [(bsymGap,symprda[symsuca[vara 1]])]) is False
-- isPatternInduCluster cls is False
wita = InduWitness clsa assk clsb :: InduWitnessa
-- isInduWitnessa wita is False
clsc = InduCluster trmf assd :: InduCluster Siga -- from example 7
clsd = InduCluster trma [] :: InduCluster Siga -- bottom for that term
witb = InduWitness clsd assd clsc  :: InduWitnessa
clse = InduCluster symGapc [(csymGap,trma)] :: InduCluster Siga -- top for that term
witc = InduWitness clsd [(csymGap,trma)] clse  :: InduWitnessa
-- isInduWitnessa witb is True, as is isInduWitnessa witc
-- calg algCAlgTrm clsc is p(s(p(s(0)))), which is indeed induClusterFor clsc, the term it is a cluster for
-- calg (algCAlg algSize) clsc is 5, i.e. just the size of the term
vecSTPose = [stposZer,singleton vtxTPosEmp] :: VecSetTPos -- (0,{e}) vector
matrixSTPose = [vecSTPosZer,vecSTPose] :: MatrixSetTPos -- (0,0),(0,{e}) matrix
calgPosition = CAlg algShift (matrixvecmul matrixSTPose) algTree :: CAlg a VecSetTPos -- position cluster algebra
-- calg calgPosition clsa is [fromList [],fromList [ε̊,1.1̊,1.1.1̅,1.1.1̊]]
-- calg calgPosition clsb is [fromList [],fromList [ε̊,1̊]], which is still ok
-- i.e. for the algebraic interpretation, only closedness of the assignment is relevant, not the pattern restr.

-- text in between
symAwayFrom :: Signature a => [a] -> [Trm a] -> Bool -- syms disjoint from non-vars in the trms
symAwayFrom ss ts = Set.null (intersection (fromList ss) (fromList (Prelude.filter (\x->not (isVar x)) (concat (map symList ts)))))
assAwayFrom :: Signature a => PfunGraphTrm a ->  PfunGraphTrm a -> Bool -- domain of former away from range of the latter
assAwayFrom g h = symAwayFrom (graphDomain g) (graphRange h)
selfAway :: Signature a => PfunGraphTrm a -> Bool -- self away predicate on graph assignments
selfAway g = assAwayFrom g g
-- selfAway assa,d,e,g-k are True,  selfAway assb,c are False (p),
-- selfAway [(asymGap,trmf)] is False, selfAway [(genvar 2,vara 1)] is True
isSelfAwayInduCluster :: Signature a => InduCluster a -> Bool
isSelfAwayInduCluster = selfAway.gapass 
symTrm :: Ord a => Trm a -> Set a -- set of symbols in a term
symTrm = alg algSym 
symGass :: Signature a => PfunGraphTrm a -> Set a -- set of free symbols in graph assignment, i.e. all except for bound variables
symGass g = fromList (concat (map (\(s,t) -> toList(difference (symTrm t) (fromList(map genvar [1..(arity s)])))) g))
symInduCluster :: Signature a => InduCluster a -> Set a -- set of free symbols in cluster, i.e. all except for bound variables
symInduCluster (InduCluster t g) = union (difference (symTrm t) (fromList (graphDomain g))) (symGass g)
maxGapIndex :: Signature a => Set a -> Int -- max of the gap indices in the set, 0 otherwise
maxGapIndex s = foldr (\s-> max (gapindex s)) 0 (toList s)
-- maxGapIndex (symGass assa) a-k,j are all 0 (no gaps in terms substited for), i yields 2 and 
-- maxGapIndex (symInduCluster (InduCluster (symGapa[symGapb[vara 2]]) [(asymGap,trmf)])) is 2 (the symGab)
renamerDom :: Signature a => Int -> [a] -> [a] -- generate domain for  gap renamer, enumerating new gaps from i+1 (should be such that bijects) 
renamerDom i = zipWith (\j x-> gengap (j+i) (arity x)) [1..] -- using as arities those of the gaps to be replaced; 
renamerRng :: Signature a => [a] -> [Trm a] -- generate range for renamer, turning symbols into terms (works for any domain, not necessarily gaps) 
renamerRng = map (\x->Fun x (map vara [1..(arity x)]))
gassTrm :: Signature a => PfunGraphTrm a -> Trm a -> Trm a -- apply graph assignment to term (should go earlier)
gassTrm g = alg (updateGraph algTrm (gassGraphTrm g))
renameGass :: Signature a => [a] -> PfunGraphTrm a -> PfunGraphTrm a
renameGass s g = zip s (graphRange g) -- rename/replace domain of graph assignment (assumes lengths of both are same)
renameInduCluster :: Signature a => [a] ->  InduCluster a -> InduCluster a  -- rename/replace domain of graph assignment in cluster, as above
renameInduCluster d (InduCluster t g) = (InduCluster (gassTrm (zip (graphDomain g) (renamerRng d)) t) (renameGass d g)) 
standardiseInduCluster :: Signature a => Int -> InduCluster a -> InduCluster a -- by renaming gaps to have indices greater than i and occurring ones 
standardiseInduCluster i c = renameInduCluster (renamerDom (max i (maxGapIndex (symInduCluster c))) (graphDomain g)) c where
  g = gapass c
selfAwayInduCluster :: Signature a => InduCluster a -> InduCluster a -- make cluster self-away
selfAwayInduCluster = standardiseInduCluster 0
-- selfAwayInduCluster clsa is (G1/1(s(G2/1(v1))),[(G1/1,p(v1)),(G2/1,p(s(v1)))])
-- whereas clsa is (X(s(Y(v1))),[(X,p(v1)),(Y,p(s(v1)))])
-- (InduCluster trmf [(asymGap,trmf)]) is (p(s(X(0))),[(X,p(s(X(0))))]), where the gapass is not self-away but
-- selfAwayInduCluster (InduCluster trmf [(asymGap,trmf)]) is (p(s(G1/1(0))),[(G1/1,p(s(X(0))))])
-- wich is self-away: isSelfAwayInduCluster (selfAwayInduCluster (InduCluster trmf [(asymGap,trmf)])) is True
-- induClusterFor (selfAwayInduCluster (InduCluster trmf [(asymGap,trmf)])) is p(s(p(s(X(0)))))
-- which is the same as induClusterFor (InduCluster trmf [(asymGap,trmf)])

-- Theorem 15
-- item 2 (e is still missing in the item and probably in the proof; still old version)
-- illustrated for cluster of example 14
-- calg calgPosition clsa is [fromList [],fromList [ε̊,1.1̊,1.1.1̅,1.1.1̊]] which is (componentwise)
--  a subset of alg algPTree (induClusterFor clsa), i.e. [fromList [ε̅],fromList [ε̊,1̅,1̊,1.1̅,1.1̊,1.1.1̅,1.1.1̊]]
-- gclsLe (internal ( calg calgPosition clsa)) (internal (alg algPTree (induClusterFor clsa))) is True
-- and the cluster is geometric isGeoCluster (internal ( calg calgPosition clsa)) (induClusterFor clsa) is True
-- item 3, transformation of position set for term to cluster
trmAt :: Trm a -> Pos -> Trm a -- return term at position, assuming pos is in the term
trmAt t [] = t
trmAt (Fun s ts) (i:p) = trmAt (ts!!(i-1)) p
trmsAt :: Trm a -> [Pos] -> [Trm a] -- return terms at positions, assuming pos are in the term
trmsAt t p = map (trmAt t) p
headSym :: Trm a -> a -- head symbol of term
headSym (Fun s _) = s
symAt :: Trm a -> Pos -> a -- return symbol at position, assuming pos is in the term
symAt t p = headSym (trmAt t p)
putAt :: Trm a -> Trm a -> Pos -> Trm a -- grafting term into a term, t[s]p, assuming pos is in the term
putAt t s [] = s
putAt (Fun h ts) s (i:p) = Fun h (aux ts i) where
  aux (x:xs) 1 = (putAt x s p):xs
  aux (x:xs) i = x:(aux xs (i-1))
putsAt :: Trm a -> [Trm a] -> [Pos] -> Trm a -- grafting terms into a term, t[vec s]P,
-- assuming P is a list of parallel positions of same length as vec s
putsAt t [] [] = t
putsAt t (s:ss) (p:ps) = putsAt(putAt t s p) ss ps
tposPos :: TPos -> Pos
tposPos (TPos p _) = p
-- putAt trma trma [1,1,1,1] is p(s(p(s(p(s(p(s(0))))))))
-- putAt (symbina[symbina[vara 1,vara 2],symzera]) trma [1,2] is f(f(v1,p(s(p(s(0))))),0)
fringeOf :: Set TPos -> Set TPos -> [Pos] -- positions in the second, which are just below the pattern in the first 
  -- not checked whether second arg is a pattern; result will be edge positions
fringeOf p t = map tposPos (toList(Set.filter (\q -> (not (member q p)) && (member (tposPrd q) p)) t))
-- fringeOf (internal (calg calgPosition clsc)) (internal (calg (algCAlg algTree) clsc)) yields fromList [1.1.1.1̅]
rootOf :: Set TPos -> Pos -- find root position of set of positions, assumes that exists, i.e. it is a pattern
rootOf = tposPos.findMin
-- contractPosTrm :: Set TPos -> Trma -> Int -> Trma
prefixDrop :: Eq a => ([a],[a]) -> ([a],[a]) -- drop common prefix of lists
prefixDrop p@((x:xs),(y:ys)) = if (x == y) then prefixDrop (xs,ys) else p
prefixDrop p = p
-- prefixDrop ([1,3,4],[1,3,7,8]) is ([4],[7,8]), prefixDrop ([1,3,4],[1,3]) is ([4],[])
leftDiv :: Eq a => [a] -> [a] -> [a] -- left division of strings, assumes first string is prefix of second
leftDiv l m = snd (prefixDrop (l,m))
-- leftDiv [1,3] [1,3,4,8] is [4,8]
isPrefix :: Eq a => [a] -> [a] -> Bool -- test for string being prefix of other
isPrefix l m = (fst (prefixDrop (l,m))) == []
posTypLe :: PosTyp -> PosTyp -> Bool
posTypLe Vtx Edg = False
posTypLe _ _ = True
tposPfxEq :: TPos -> TPos -> Bool -- prefix (not necessarily proper)
tposPfxEq (TPos p t) (TPos q s) = aux (prefixDrop (p,q)) where 
  aux ([],[]) = posTypLe t s
  aux ([],(_:_)) = True
  aux _ = False
abstractBorderpos :: Pos -> [Pos] -> TPos -> TPos
 --  abstract root,fringe into a node for a set of positions
  -- assumption is that root is prefix of all positions in the fringe, fringe are parallel vertex pos
abstractBorderpos r f p'@(TPos p t) = if (tposPfxEq (TPos r Vtx) p') then (aux 1 f) else p' where
  aux i (q:f') = if (tposPfxEq (TPos q Edg) p') then (TPos (r++(i:(leftDiv q p))) t) else (aux (i+1) f')
  aux i [] = TPos r Vtx -- i.e. abstract all positions in the pattern to the root (vertex)
abstractBorderPos :: Pos -> [Pos] -> Set TPos -> Set TPos --  abstract root,fringe into a node for a set of positions
abstractBorderPos r f p = fromList(map (abstractBorderpos r f) (toList p))
abstractPatPos :: Trm a -> Set TPos -> Set TPos -> Set TPos -- abstract pattern (set of positions) in a term into a node 
abstractPatPos t p s = abstractBorderPos r f s where
  r = rootOf p
  f = fringeOf p (internal (alg algTree t))
-- abstractPatPos trma (singleton (TPos [1] Vtx)) (singleton (TPos [1] Vtx)) give empty list
abstractTrmPosi :: Signature a => Trm a -> Set TPos -> Int -> InduCluster a -- abstract pattern (set of positions) in a term into Gap i
abstractTrmPosi t p i = InduCluster (putAt t (Fun h tf) r) [(h,putsAt tr v rf)] where
  r = rootOf p
  f = fringeOf p (internal (alg algTree t))
  tr = trmAt t r
  tf = trmsAt t f
  rf = map (leftDiv r) f 
  a = length f
  h = (gengap i a)
  v = map vara [1..a]
-- test abstraction
trmi = symsuca[symbina[symbina[symprda[symzera],vara 1],vara 2]]
posa = fromList [(TPos [1] Vtx),(TPos [1,1] Edg),(TPos [1,1] Vtx)]
-- trmi is s(f(f(p(0),v1),v2))
-- abstractTrmPosi trmi posa 2 is ( s(Y/3(p(0),v1,v2)) | [(Y/3,f(f(v1,v2),v3))] )
-- abstractPatPos trmi posa (internal (alg algTree trmi)) is
-- [ε̊,1̅,1̊,1.1̅,1.1̊,1.1.1̅,1.1.1̊,1.2̅,1.2̊,1.3̅,1.3̊]
-- which are the internal positions of s(Y/3(p(0),v1,v2))
geoInduClusteri :: Signature a => GeoCluster a -> Int -> (InduCluster a,Int)
geoInduClusteri (GeoCluster t p) i = aux ((InduCluster t []),i',ps) where
  i' = (max (maxGapIndex (alg algSym t)) i)+1
  ps = toList(gclsPartition p)
  aux (c,k,[]) = (c,k)
  aux ((InduCluster t' g),j,(q:qs)) = aux ((InduCluster (skeleton a) (g++(gapass a))),j+1,qs') where
    a = abstractTrmPosi t' q j
    qs' = map (abstractPatPos t' q) qs
geoInduCluster :: Signature a => GeoCluster a -> InduCluster a
geoInduCluster c = fst (geoInduClusteri c 0)
induGeoCluster :: Signature a => InduCluster a -> GeoCluster a
induGeoCluster c = GeoCluster (induClusterFor c) (internal (calg calgPosition c))
-- recall clsa is ( X(s(Y(v1))) | [(X,p(v1)),(Y,p(s(v1)))] )
-- induGeoCluster clsa gives ( p(s(p(s(v1)))) | fromList [ε̊,1.1̊,1.1.1̅,1.1.1̊] )
-- and back again geoInduCluster (induGeoCluster clsa) yields ( X(s(Y(v1))) | [(X,p(s(v1))),(Y,p(v1))] ) again
geoInduWitnessi :: Signature a => GeoWitness a -> Int -> (Int -> Int) -> (InduWitness a,Int)
geoInduWitnessi (GeoWitness l t r) i f = aux ((InduCluster t []),i',ls,rs) where
  i' = max ((max (maxGapIndex (alg algSym t)) i)+1) 1
  ls = toList(gclsPartition l)
  rs = toList(gclsPartition r)
  aux ((InduCluster t' g),j,(q:qs),os) = aux ((InduCluster (skeleton a) (g++(gapass a))),j+1,qs',os') where
    a = abstractTrmPosi t' q j
    qs' = map at qs
    os' = map at os
    at  = abstractPatPos t' q
  aux (c,k,[],ns) = aux' (c,(InduCluster (skeleton c) []),max (f k) 1,ns) where
    aux' (d,(InduCluster u' h),s,(m:ms)) = aux' (d,(InduCluster (skeleton b) (h++(gapass b))),s+1,ms') where
      b = abstractTrmPosi u' m s
      ms' =  map (abstractPatPos u' m) ms
    aux' (d,e,x,y) = ((InduWitness d (gapass e) (InduCluster (skeleton e) e')),x) where
      e' = map (\(g1,t1) -> (g1,gassTrm (gapass d) t1)) (gapass e)
geoInduWitness :: Signature a => GeoWitness a -> InduWitness a
geoInduWitness w = fst (geoInduWitnessi w 0 (\x -> 0))
induGeoWitness :: Signature a => InduWitness a -> GeoWitness a
induGeoWitness (InduWitness l w r) = (GeoWitness l' t r') where
  l' = clspos gl
  r' = clspos (induGeoCluster r)
  t =  clstrm gl
  gl = induGeoCluster l
-- witb is ( p(s(p(s(0)))) | [] ) ⊑[(X,p(s(v1)))] ( p(s(X(0))) | [(X,p(s(v1)))] )
-- induGeoWitness witb is fromList [] ⊆p(s(p(s(0)))) fromList [1.1̊,1.1.1̅,1.1.1̊]
-- and geoInduWitness (induGeoWitness witb) yields the first again
trmk = symsuca[symbina[symprda[symzera],vara 2]]
trml = symsuca[symGapd[symGapa[symzera],vara 2]]
trmm = symsuca[symGape[symzera,vara 2]]
assf = [(dsymGap,symbina[vara 1,vara 2]),(asymGap,symprda[vara 1])]
assl = [(esymGap,symbina[symprda[vara 1],vara 2])]
assm = [(esymGap,symGapd[symGapa[vara 1],vara 2])]
witd = InduWitness (InduCluster trml assf) assm (InduCluster trmm assl)
-- geoInduWitness (induGeoWitness witd) yields
-- ( s(X/2(Y(0),v2)) | [(Y,p(v1)),(X/2,f(v1,v2))] ) ⊑[(X/2,X/2(Y(v1),v2))] ( s(X/2(0,v2)) | [(X/2,f(p(v1),v2))] )

-- clsf = InduCluster symGapa

-- text in between
-- lattice operations on geometric clusters
geoClusterBot :: Trm a -> GeoCluster a -- bottom
geoClusterBot t = GeoCluster t gclsBot
geoClusterLub :: GeoCluster a -> GeoCluster a -> GeoCluster a -- lub, assumes same terms
geoClusterLub c d = GeoCluster (clstrm c) (gclsLub (clspos c) (clspos d))
geoClusterGlb :: GeoCluster a -> GeoCluster a -> GeoCluster a -- glb, assumes same terms
geoClusterGlb c d = GeoCluster (clstrm c) (gclsGlb (clspos c) (clspos d))
geoClusterTop :: Signature a => Trm a -> GeoCluster a -- top
geoClusterTop t = GeoCluster t (gclsTop t) 
induClusterBot :: Signature a => Trm a -> InduCluster a -- bottom
induClusterBot t = InduCluster t []
induClusterLub :: Signature a => InduCluster a -> InduCluster a -> InduCluster a -- lub, via geometric patterns
induClusterLub c d = geoInduCluster (geoClusterLub (induGeoCluster c) (induGeoCluster d))
induClusterGlb :: Signature a => InduCluster a -> InduCluster a -> InduCluster a -- glb, via geometric patterns
induClusterGlb c d = geoInduCluster (geoClusterGlb (induGeoCluster c) (induGeoCluster d))
induClusterTop :: Signature a => Trm a -> InduCluster a -- bottom
induClusterTop t = geoInduCluster (geoClusterTop t)
trmj = symsuca[symprda[symzera]]
gclsa = GeoCluster trmj posa
gclsb = GeoCluster trmj (fromList([(TPos [] Vtx),(TPos [1] Edg),(TPos [1] Vtx)]))
iclsa = geoInduCluster gclsa
iclsb = geoInduCluster gclsb
-- iclsa is ( s(X/0) | [(X/0,p(0))] )
-- iclsb is ( X(0) | [(X,s(p(v1)))] )
-- induClusterLub iclsa iclsb is ( X/0 | [(X/0,s(p(0)))] )
-- induClusterGlb iclsa iclsb is ( s(X(0)) | [(X,p(v1))] )
cleanInduCluster :: Signature a => InduCluster a -> InduCluster a -- erase spurious binders
cleanInduCluster (InduCluster s g) = (InduCluster s g') where
  g' = Prelude.filter (\(x,y)-> member x l) g
  l = alg algSym s
-- cleanInduCluster (InduCluster symzera assa) yields ( 0 | [] )
-- can also be done by translating to geometric cluster and back again
-- that, by the way, also standardises
-- that also unshares assignments, i.e. making an assignment a linear one

-- Definition 16
geoPatternIn :: GeoCluster a -> GeoCluster a -> Bool -- test whether geometric pattern in a cluster
geoPatternIn (GeoCluster t p) (GeoCluster s q) = member p (gclsPartition q)
induClusterIn :: Signature a => InduCluster a -> InduCluster a -> Bool
induClusterIn c d = geoPatternIn (induGeoCluster c) (induGeoCluster d)
gclsc =  GeoCluster trmj (fromList([(TPos [1,1] Vtx),(TPos [] Vtx),(TPos [1] Edg),(TPos [1] Vtx)]))
-- geoPatternIn gclsa gclsb is False, partial overlap
-- geoPatternIn gclsb gclsb is True, pattern so in itself.
-- geoPatternIn gclsb gclsc is True, p(0) among s and p(0)
-- geoPatternIn gclsc gclsc is False, not a (single) pattern, but two
-- geoPatternIn gclsa gclsc is False, s proper subpattern of s(p(v1))
isBot (GeoCluster _ p) = Set.null p
isTop (GeoCluster t p) = (p == internal (alg algPTree t)) -- top, all internal positions (so variable, or variable instance of linear top)
isLinear (GeoCluster t p) =  (l == nvars (length l)) where l = varsList t -- check for linearity, f(v1 ... vn) with f any symbol.
geoPairCritical :: Signature a => (GeoCluster a,GeoCluster a) -> Bool -- test whether two patterns are critical
-- to revisit : added here that variables, if any, are standard, to get uniqueness, should work out (better even i guess)
-- no, variables may be there! paper was/is correct, test removed again
geoPairCritical (c,d) = (not (isBot c)) && (not (isBot d)) && isTop (geoClusterLub c d)  -- && (isLinear (geoClusterLub c d)) 
gclsd = GeoCluster (symbina[vara 1,vara 1]) (fromList [(TPos [] Vtx)])
geoPairOverlap :: (GeoCluster a,GeoCluster a) -> Bool
geoPairOverlap (c,d) = not (isBot (geoClusterGlb c d))
geoPairEmpty :: (GeoCluster a,GeoCluster a) -> Bool -- check whether one of the steps is empty
geoPairEmpty (c,d) = isBot c || isBot d -- simplifies paper (which is correct, but rather silly; implemented it wrongly at first; added negation)
geoPairSize :: Signature a => (GeoCluster a,GeoCluster a) -> Int 
geoPairSize (c,d) = alg algPSize (skeleton (geoInduCluster (geoClusterLub c d)))

-- page 7

-- Definition 18
tposLftEq :: TPos -> TPos -> Bool -- left or equal relation on typed positions
tposLftEq (TPos p t) (TPos q s) = case (prefixDrop (p,q)) of
  ([],[]) -> t == s
  ((i:p'),(j:q')) -> i < j
  _ -> False
tposLft  :: TPos -> TPos -> Bool
tposLft p q = (tposLftEq p q) && (not (p ==q))
tposPfx :: TPos -> TPos -> Bool -- proper prefix relation on typed positions
tposPfx p q = (tposPfxEq p q) && (not (p == q))
tposLo ::  TPos -> TPos -> Bool -- proper left--outer relation on typed positions
tposLo p q = (tposPfx p q) || (tposLft p q)
tposLoEq :: TPos -> TPos -> Bool  -- left-outer or equal relation on typed positions
tposLoEq p q = (tposLo p q) || (p == q)
-- using compare would both be faster and more consise. anyway, we follow the paper for now

-- text in between
-- extension of order to patterns, via their root; here for geometric representation as sets only
patPos :: Set TPos -> TPos --we do not test whether it's in fact a pattern
patPos = findMin  -- root is minimal element;
patGeoPos = patPos.clspos
patLft p q = tposLft (patPos p) (patPos q)
patLftEq p q = tposLftEq (patPos p) (patPos q)
patPfx p q = tposPfx (patPos p) (patPos q)
patPfxEq p q = tposPfxEq (patPos p) (patPos q)
patLo p q = tposLo (patPos p) (patPos q)
patLoEq p q = tposLoEq (patPos p) (patPos q)
patGeoPfx p q = patPfx (clspos p) (clspos q)

-- Definition 19
geoPairOutIn :: (GeoCluster a,GeoCluster a) -> Bool 
geoPairOutIn (c,d) = patGeoPfx c d -- these definitions assume fst,snd  are indeed overlapping
geoPairInOut (c,d) = patGeoPfx d c
geoPairOverlay (c,d) = (clspos d) == (clspos c)
geoPairIn :: (GeoCluster a,GeoCluster a) ->  (GeoCluster a,GeoCluster a) -> Bool
  -- test pair of patterns in pair of clusters 
geoPairIn (p,q) (c,d) = (geoPatternIn p c) && (geoPatternIn q d)

-- text in between
geoPairFstOuter (c,d) = (patPfxEq (clspos c) (clspos d)) 
geoPairSndOuter (c,d) = geoPairFstOuter (d,c)
geoPairMax :: (GeoCluster a, GeoCluster a) -> GeoCluster a
geoPairMax (c,d) = if (patPfx (clspos c) (clspos d)) then d else c
geoPairPfx :: (GeoCluster a, GeoCluster a) -> (GeoCluster a, GeoCluster a) -> Bool
geoPairPfx p q = patPfx (clspos (geoPairMax p)) (clspos (geoPairMax q))
geoOverlapPairs :: (GeoCluster a,GeoCluster a) -> [(GeoCluster a,GeoCluster a)] -- list of overlapping pairs of patterns for two clusters
geoOverlapPairs (c,d) = [((GeoCluster (clstrm c) p),(GeoCluster (clstrm d) q)) | p<-(toList(gclsPartition (clspos c))),q <-(toList(gclsPartition (clspos c))),(geoPairOverlap ( (GeoCluster (clstrm c) p),(GeoCluster (clstrm d) q)))] 
maxInList :: a -> (a -> a -> Bool) -> [a] -> Bool -- test whether x is maximal in list, assuming the relation r is a `less-than' relation
maxInList x r = all (\y->(not (r x y)))
geoPairInner :: Eq a => (GeoCluster a, GeoCluster a) -> (GeoCluster a, GeoCluster a) -> Bool
geoPairInner (p,q) (c,d) = (elem (p,q) l) && (maxInList (p,q) geoPairPfx l) where
  l = geoOverlapPairs (c,d)
posX :: Signature a => InduCluster a -> a -> Set TPos
posX (InduCluster t g) s = internal p where
  gt = Prelude.filter (\x -> s == (fst x)) g
  gf = Prelude.filter (\x -> not (s == (fst x))) g
  t' = gassTrm gf t
  p = calg calgPosition (InduCluster t' gt)


induInnerOverlapPairs :: Signature a => (InduCluster a,InduCluster a) -> ((a,a),Ordering) -- some gap-pair constituting inner overlap pairs
induInnerOverlapPairs (c,d) = (iop,if (patPfx pc pd) then LT else (if (patPfx pd pc) then GT else EQ)) where -- assumed c,d are normalised (no shared/erased gaps)
  t = induClusterFor c
  op = [(g,h) | g <- graphDomain (gapass c), h <- graphDomain (gapass d), (geoPairOverlap ( (GeoCluster t (posX c g)),(GeoCluster t (posX d h))))]
  iop = head (Prelude.filter (\(p,p') -> all (\(q,q') -> not (geoPairPfx (GeoCluster t (posX c p),GeoCluster t (posX d p')) (GeoCluster t (posX c q),GeoCluster t (posX d q')))) op) op)
  pc = posX c (fst iop) -- left pattern of inner overlap
  pd = posX d (snd iop) -- right pattern of inner overlap
-- Example 20
posb = [TPos [] Vtx,TPos [1] Edg,TPos [1] Vtx]
posc = [TPos [1] Vtx,TPos [1,1] Edg,TPos [1,1] Vtx]
posd = [TPos [1,1] Vtx,TPos [1,1,1] Edg,TPos [1,1,1] Vtx]
pose = [TPos [] Vtx]
patpi = GeoCluster trma (fromList posb)
patrho = GeoCluster trma (fromList posc)
patomikron = GeoCluster trma (fromList posd)
patkappa = GeoCluster trma (fromList pose)
-- patGeoPos patpi is ε̊
-- patGeoPos patrho is 1̊
-- patGeoPos patomikron is 1.1̊
-- patGeoPfx patpi patrho is True
-- patGeoPfx patrho patomikron is True
-- patGeoPfx patrho patpi is False
-- patGeoPfx patrho patrho is False
-- geoPairOverlap (patpi,patomikron) is False
-- geoPairPfx (patpi,patrho) (patomikron,patrho) is True (converse is False

-- Definition 22
type PfunGraphCluster a = PfunGraph a (InduCluster a) 
type PfunGraphClustera = PfunGraphCluster Siga
clusterTrmPfunGraph :: PfunGraphCluster a -> PfunGraphTrm a
clusterTrmPfunGraph g = zip (graphDomain g) (map skeleton (graphRange g))
disjoint :: Eq a => [a] -> [a] -> Bool
disjoint l m = not(any (\x->elem x m) l)
pairwiseDisjoint :: Eq a => [[a]] -> Bool
pairwiseDisjoint [] = True
pairwiseDisjoint (x:xs) = (all (disjoint x) xs) && (pairwiseDisjoint xs)
clsAwayFrom :: Signature a => InduCluster a -> PfunGraphCluster a -> Bool
clsAwayFrom c ac = (selfAway a) && (pairwiseDisjoint (dc:dcs)) where
  a = clusterTrmPfunGraph ac
  dcs = map (graphDomain.gapass.snd) ac
  dc = graphDomain (gapass c)
clsCompose :: Signature a => InduCluster a -> PfunGraphCluster a -> InduCluster a
clsCompose (InduCluster s g) ac = (InduCluster (gassTrm ms s) (g++gs)) where
  ms = clusterTrmPfunGraph ac
  gs = concat (map (gapass.snd) ac)
-- renaming version of compose, where the gaps in the former are renamed away from those in the latter
clsSaferCompose :: Signature a => InduCluster a -> PfunGraphCluster a -> InduCluster a
clsSaferCompose c l = clsCompose cawayfroml l where
  cawayfroml = standardiseInduCluster i c -- rename to gaps above i, where i is max of gaps in l (both dom,ran)
  i = foldl (\j -> \(s,t) -> max (max (gapindex s) (maxGapIndex (symInduCluster t))) j) 0 l
            

-- Example 23
clsf = InduCluster (symGapa[symGapb[symzera]])
                   [(asymGap,symprda[symsuca[vara 1]]),(bsymGap,symprda[symsuca[vara 1]])]
clsg = InduCluster (symGapa[vara 4]) [(asymGap,symprda[symsuca[vara 1]])]
clsh = InduCluster (symGapb[vara 1]) [(bsymGap,symprda[symsuca[vara 1]])]
-- clsAwayFrom clsg [(Var 4,clsh)] is True
clsg1 = InduCluster (symGapa[vara 1]) [(asymGap,symprda[symsuca[vara 1]])]
-- still is True??, maybe ok, for  Var 1,  check. i now think so; bound.

-- Lemma 24
-- induClusterFor clsg is p(s(v4))
-- induClusterFor clsh is p(s(v1))
-- gassTrm [(Var 4, induClusterFor clsh)] (induClusterFor clsg) is p(s(p(s(v1))))
-- clsCompose clsg [(Var 4,clsh)] is ( X(Y(v1)) | [(X,p(s(v1))),(Y,p(s(v1)))] ) and
-- induClusterFor (clsCompose clsg [(Var 4,clsh)]) is p(s(p(s(v1))))
-- gassTrm [(Var 1, induClusterFor clsh)] (induClusterFor clsg1) is p(s(p(s(v1))))
-- clsCompose clsg1 [(Var 1,clsh)] is ( X(Y(v1)) | [(X,p(s(v1))),(Y,p(s(v1)))] )
-- induClusterFor (clsCompose clsg1 [(Var 1,clsh)]) is p(s(p(s(v1)))) still.

-- Section 3.3
-- page 8
-- Definition 25
type TRule a = PfunGraph a (Trm a,Trm a)
data TRS a = TRS { rules :: TRule a } deriving (Eq)
lhs :: Signature a => TRS a -> a -> Trm a
lhs z = updateGraph trmAss (map (\(s,p) -> (s,fst p)) (rules z))
rhs :: Signature a => TRS a ->  a -> Trm a 
rhs z = updateGraph trmAss (map (\(s,p) -> (s,snd p)) (rules z))
dom :: Signature a => TRS a -> [a]
dom z = graphDomain (rules z)
trsInv :: Signature a => TRS a -> TRS a 
trsInv z = TRS (zip (graphDomain r) (map (\(x,y)->(y,x)) (graphRange r))) where r = rules z -- inverse (pseudo) TRS
isRuleSymbol :: Signature a => a -> Bool
isRuleSymbol s = case (stype s) of
  TRule -> True
  _ -> False
isFOTrm :: Signature a => Trm a -> Bool -- test whether term is fo-term, i.e. no rule or gap symbols
isFOTrm (Fun s ts) = not ((\x->isRuleSymbol x || isGap x) s) && all isFOTrm ts
isRule :: Signature a => TRS a -> a -> Bool
isRule z s = isRuleSymbol s && not (isVar (trmHead l)) && isSubsetOf (alg algVar r) lv && isSubsetOf lv (fromList(nvars (arity s)))
  && isTrm l && isTrm r && isFOTrm l && isFOTrm r where
  lv = alg algVar l
  l = lhs z s
  r = rhs z s
isLeftLinearRule :: Signature a => TRS a -> a -> Bool -- check a rule being left-linear (doesn't check whether it's a rule)
isLeftLinearRule z s = isLinearList (varsList (lhs z s))
isStandardRule :: Signature a => TRS a -> a -> Bool
isStandardRule z s = isStandard (lhs z s)
instance Show a => Show (TRS a) where
  show t = "(RULES \n"++(concat (map (\(r,p)->(show r)++": "++(show (fst p))++" -> "++(show (snd p))++"\n") (rules t)))++")\n"

isTRS :: Signature a => TRS a -> Bool -- check whether rules satisfy TRS constraints, assign to rule symbols only,
-- lhs not a var and vars rhs contained in vars lhs, and they are contained in v1 ... v(arity rulesymbol)
isTRS z = all (isRule z) (dom z)
isStandardLLTRS  :: Signature a => TRS a -> Bool -- check whether also our constrants, left-linearity and standardness hold
isStandardLLTRS z = isTRS z && (all (\r-> isLeftLinearRule z r && isStandardRule z r) (dom z))

-- Example 26
atrs :: TRS Siga
atrs = TRS [(crulzer,(symzera,symzera))]  -- just to see how it works
btrs :: TRS Siga 
btrs = TRS [(arulone,(symprda[symsuca[vara 1]],vara 1)),(brulone,(symsuca[symprda[vara 1]],vara 1))]
ctrs :: TRS Siga
ctrs = TRS [(arulone,(symprda[vara 1],symbina[vara 1,vara 1]))]
-- lhs btrs is [(ρ,p(s(v1))),(θ,s(p(v1)))]
-- rhs btrs is [(ρ,v1),(θ,v1)]
-- isStandardLLTRS atrs and btrs are true
-- isStandardLLTRS (TRS [(symzer,(symzera,symzera))]) is false, not a rule symbol
-- isTRS (TRS [(crulzer,(vara 1,vara 1))]) is false
-- isTRS (TRS [(crulone,(vara 1,vara 1))]) is false, lhs var
-- isTRS (TRS [(crulone,(symzera,vara 1))]) is false rhs not in lhs
-- isTRS (TRS [(crulone,(symprda[vara 1],symzera))]) is ok
-- isStandardLLTRS  (TRS [(crulone,(symbina[vara 1,vara 1],symzera))]) is false
dtrs :: TRS Siga
dtrs = TRS [(arulzer,(symzeraa,symzerba)),
            (brulzer,(symzeraa,symzerca)),
            (crulzer,(symzerba,symzerca)),
            (drulzer,(symzerca,symzerba))]

-- Definition 27
isSOTrm :: Signature a => Trm a -> Bool -- test whether term is so-term, i.e. no rule symbols
isSOTrm (Fun s ts) = not ((\x->isRuleSymbol x) s) && all isSOTrm ts
isMultistep :: Signature a => TRS a -> InduCluster a -> Bool
isMultistep z c = isPatternInduCluster c && isSOTrm (skeleton c) && all (\s->lhs z s==trmAss s) (graphDomain (gapass c))
isStep z c = isMultistep z c && length (graphDomain (gapass c)) == 1 -- assume multistep is normalised, i.e. that gap does occur
-- lhs and rhs clusters of multisteps, by applying lhs and rhs to the assignment
lhsass :: Signature a => TRS a -> InduCluster a -> InduCluster a
lhsass z (InduCluster s g) = (InduCluster s (map (\(x,y)->(x,alg (assAlgTrm (lhs z)) y)) g))
rhsass :: Signature a => TRS a -> InduCluster a -> InduCluster a
rhsass z (InduCluster s g) = (InduCluster s (map (\(x,y)->(x,alg (assAlgTrm (rhs z)) y)) g))
src :: Signature a => TRS a -> InduCluster a -> Trm a
src z c = induClusterFor (lhsass z c)
tgt z c = induClusterFor (rhsass z c)
tgt :: Signature a => TRS a -> InduCluster a -> Trm a
proofterm :: Signature a => InduCluster a -> Trm a 
proofterm c = induClusterFor c
data Multistep a = Multistep {
  forward :: Bool,
  whole :: Bool,
  mtrs :: (TRS a),
  mstp :: (InduCluster a)
}
isEmpty :: Signature a => InduCluster a -> Bool
isEmpty c = (gapass c) == []
showTStep :: Signature a => TRS a -> InduCluster a -> String -- show smallest among, empty, single, multistep; to be done, include parallel
showTStep z c = if (isEmpty bbc) then "=" else (if (isStep z bbc) then "" else "o") where bbc = bb c
instance Signature a => Show (Multistep a) where
  show (Multistep True  w z c) = (if w then (show (src z c)) else "")++" -"++(showTStep z c)++"->"++(show (proofterm c))++" "++(show (tgt z c))
  show (Multistep False w z c) = (if w then (show (tgt z c)) else "")++" "++(show (proofterm c))++"<-"++(showTStep z c)++"- "++(show (src z c))
bb ::  Signature a => InduCluster a ->  InduCluster a -- being there and back again
bb = geoInduCluster.induGeoCluster -- normalise resulting cluster into a linear one by translating to positions and back again
-- the point is that the coinduced step may have replicated gaps in its skeleton, which are taken care of in this way
split :: Signature a => (a -> Bool)-> TRS a -> InduCluster a -> (InduCluster a,InduCluster a)
split f z (InduCluster s g) = ((InduCluster st gt),bb (InduCluster sf gf)) where
  gt = Prelude.filter (f.fst) g
  gf = Prelude.filter (\x->not (f (fst x))) g
  st = alg (assAlgTrm (lhs z)) (gassTrm gf s)
  sf = alg (assAlgTrm (rhs z)) (gassTrm gt s)
splitOn :: Signature a => [a] -> TRS a -> InduCluster a -> (InduCluster a,InduCluster a)
splitOn l = split (\x -> elem x l)
induced :: Signature a => TRS a -> a -> InduCluster a -> InduCluster a
induced z s c = fst(splitOn [s] z c)
coinduced :: Signature a => TRS a -> a -> InduCluster a -> InduCluster a
coinduced z s c = snd(splitOn [s] z c)

-- Example 28
aStp = InduCluster (symGapa[symGapb[symzera]]) [(asymGap,rulonea[vara 1]),(bsymGap,rulonea[vara 1])]
-- isMultistep atrs aStp is true
-- isStep atrs aStp is false (two gaps)
-- lhsMultistep btrs aStp is ( X(Y(0)) | [(X,p(s(v1))),(Y,p(s(v1)))] )
-- rhsMultistep btrs aStp is ( X(Y(0)) | [(X,v1),(Y,v1)] )
-- src btrs aStp
-- tgt btrs aStp
-- Multistep True True btrs aStp is p(s(p(s(0)))) -o->ρ(ρ(0)) 0
-- splitOn [asymGap] btrs aStp is (( X(p(s(0))) | [(X,ρ(v1))] ),( X(0) | [(X,ρ(v1))] ))
-- splitOn [bsymGap] btrs aStp is (( p(s(Y(0))) | [(Y,ρ(v1))] ),( X(0) | [(X,ρ(v1))] ))
-- splitOn [asymGap] ctrs aStp is (( X(p(0)) | [(X,ρ(v1))] ),( f(X(0),Y(0)) | [(Y,ρ(v1)),(X,ρ(v1))] ))
-- splitOn [bsymGap] ctrs aStp is (( p(Y(0)) | [(Y,ρ(v1))] ),( X(f(0,0)) | [(X,ρ(v1))] ))
-- Multistep True True ctrs aStp is p(p(0)) -o->ρ(ρ(0)) f(f(0,0),f(0,0))
-- splitOn [asymGap] btrs aStp is (( X(p(s(0))) | [(X,ρ(v1))] ),( X(0) | [(X,ρ(v1))] ))
-- splitOn [bsymGap] btrs aStp is (( p(s(Y(0))) | [(Y,ρ(v1))] ),( X(0) | [(X,ρ(v1))] ))
-- splitOn [asymGap] ctrs aStp is (( X(p(0)) | [(X,ρ(v1))] ),( f(X(0),Y(0)) | [(Y,ρ(v1)),(X,ρ(v1))] ))
-- splitOn [bsymGap] ctrs aStp is (( p(Y(0)) | [(Y,ρ(v1))] ),( X(f(0,0)) | [(X,ρ(v1))] ))
-- induced ctrs asymGap aStp is ( X(p(0)) | [(X,ρ(v1))] )
-- coinduced ctrs asymGap aStp is ( f(X(0),Y(0)) | [(Y,ρ(v1)),(X,ρ(v1))] )

-- text in between
data Reduction a = Reduction {
  rforward :: Bool,
  rwhole :: Bool,
  rtrs :: (TRS a),
  rsrc :: Trm a,
  rred :: [(InduCluster a)]
}
instance Signature a => Show (Reduction a) where
  show (Reduction True  True  z i cs) = (show i)++(show (Reduction True False z i cs))
  show (Reduction True  False _ _ []) = ""
  show (Reduction True  False z i (c:cs)) = (show (Multistep True False z c))++(show (Reduction True False z i cs))
  show (Reduction False True  z i cs) = (show i)++(show (Reduction False False z i cs))
  show (Reduction False False _ _ []) = ""
  show (Reduction False False z i cs) = (show (Multistep False False z (last cs)))++(show (Reduction False False z i (init cs)))
dirReduction :: Signature a => Bool -> TRS a -> [InduCluster a] -> Reduction a
dirReduction d z l@(c:cs) = Reduction d True z (src z c) l
-- dirReduction True ctrs [induced ctrs asymGap aStp,coinduced ctrs asymGap aStp]
-- p(p(0)) ->ρ(p(0)) f(p(0),p(0)) -o->f(ρ(0),ρ(0)) f(f(0,0),f(0,0))
-- dirReduction False ctrs [induced ctrs asymGap aStp,coinduced ctrs asymGap aStp] 
-- f(p(0),p(0)) ρ(p(0))<- f(f(0,0),f(0,0)) f(ρ(0),ρ(0))<-o- p(p(0))
development :: Signature a => ([a]->a) -> TRS a -> InduCluster a -> Reduction a
development f z c = (Reduction True True z (src z c) (aux c)) where
  aux (InduCluster _ []) = []
  aux e@(InduCluster _ g) = (fst d):(aux (snd d)) where
    d = splitOn [f (graphDomain g)] z e
outermostDevelopment :: Signature a => TRS a -> InduCluster a -> Reduction a
outermostDevelopment z c = development head z (bb c)
innermostDevelopment :: Signature a => TRS a -> InduCluster a -> Reduction a
innermostDevelopment z c = development last z (bb c)
-- innermostDevelopment ctrs aStp is p(p(0)) ->p(ρ(0)) p(f(0,0)) ->ρ(f(0,0)) f(f(0,0),f(0,0))
-- outermostDevelopment ctrs aStp is p(p(0)) ->ρ(p(0)) f(p(0),p(0)) ->f(ρ(0),p(0)) f(f(0,0),p(0)) ->f(f(0,0),ρ(0)) f(f(0,0),f(0,0))
bStp = InduCluster (symGapa[symGapb[symGapf[symzera]]]) [(asymGap,rulonea[vara 1]),(bsymGap,rulonea[vara 1]),(fsymGap,rulonea[vara 1])]
-- outermostDevelopment ctrs bStp is p(p(p(0))) ->ρ(p(p(0))) f(p(p(0)),p(p(0))) ->f(ρ(p(0)),p(p(0))) f(f(p(0),p(0)),p(p(0))) ->f(f(ρ(0),p(0)),p(p(0))) f(f(f(0,0),p(0)),p(p(0))) ->f(f(f(0,0),ρ(0)),p(p(0))) f(f(f(0,0),f(0,0)),p(p(0))) ->f(f(f(0,0),f(0,0)),ρ(p(0))) f(f(f(0,0),f(0,0)),f(p(0),p(0))) ->f(f(f(0,0),f(0,0)),f(ρ(0),p(0))) f(f(f(0,0),f(0,0)),f(f(0,0),p(0))) ->f(f(f(0,0),f(0,0)),f(f(0,0),ρ(0))) f(f(f(0,0),f(0,0)),f(f(0,0),f(0,0)))
data LocalPeak a = LocalPeak {
  lptrs :: (TRS a),
  lmstp :: (InduCluster a),
  rmstp :: (InduCluster a)
} deriving (Eq)
instance Signature a => Show (LocalPeak a) where
   show (LocalPeak z c d) = (show (Multistep False True z c))++(show (Multistep True False z d))
-- LocalPeak ctrs aStp aStp is f(f(0,0),f(0,0)) ρ(ρ(0))<-o- p(p(0)) -o->ρ(ρ(0)) f(f(0,0),f(0,0))
-- definitions for rules that factor through their left-hand sides
lpeakGeoPair :: Signature a => LocalPeak a -> (GeoCluster a,GeoCluster a)
lpeakGeoPair (LocalPeak z l r) = (induGeoCluster (lhsass z l),induGeoCluster (lhsass z r))
lpeakCritical :: Signature a => LocalPeak a -> Bool
lpeakCritical = geoPairCritical.lpeakGeoPair
lpeakOverlap :: Signature a => LocalPeak a -> Bool
lpeakOverlap = geoPairOverlap.lpeakGeoPair
lpeakEmpty :: Signature a => LocalPeak a -> Bool
lpeakEmpty = geoPairEmpty.lpeakGeoPair
lpeakSize :: Signature a => LocalPeak a -> Int 
lpeakSize = geoPairSize.lpeakGeoPair
lpeakLub p = geoClusterLub (fst p') (snd p') where p' = lpeakGeoPair p
lpeakGlb p = geoClusterGlb (fst p') (snd p') where p' = lpeakGeoPair p
-- for the triviality check we need the righthand sides 
lpeakTrivial :: Signature a => LocalPeak a ->Bool -- test whether peak t <-o- s -o-> u is trivial, i.e. t = u
lpeakTrivial (LocalPeak z l r) = (tgt z l == tgt z r) -- doesn't check wehether multisteps are in fact single steps
-- lpeakTrivial _ = False
-- swap commenting out for omitting triviality check

aPeak = LocalPeak ctrs aStp aStp
-- lpeakGeoPair aPeak is (( p(p(0)) | fromList [ε̊,1̊] ),( p(p(0)) | fromList [ε̊,1̊] ))
-- lpeakCritical aPeak is False (disconnected components)
-- lpeakOverlap aPeak is True (do have overlap)
-- lpeakSize aPeak is 3
-- lpeakLub aPeak is ( p(p(0)) | fromList [ε̊,1̊] )
-- lpeakGlb aPeak is ( p(p(0)) | fromList [ε̊,1̊] )

-- Lemma 30
-- item 1 
lpeakInstance :: Signature a => LocalPeak a -> PfunGraphTrm a -- variable substitution
-- for peak with size >= 1
lpeakInstance (LocalPeak z l r) = zip (nvars (length v)) v where v = trmArgs (skeleton l)
-- item 2
varAwayFrom :: Signature a => [a] -> Int -- generate first var not in the list
varAwayFrom l = aux 1 where
  aux i = if (elem (genvar i) l) then aux (i+1) else i
indexList :: (a -> Bool) -> [a] -> Int -- yield index of some element satisying predicate 
indexList f l = aux 1 l where
  aux i (x:xs) = if (f x) then i else (aux (i+1) xs)
lpeakDecompose :: Signature a => LocalPeak a -> (LocalPeak a,a,LocalPeak a) -- decompose local
-- multistep peak with size >= 1 into two smaller such peaks
lpeakDecompose p@(LocalPeak z l r) = ((LocalPeak z ltop rtop),v,(LocalPeak z lbot rbot)) where
  lg = induGeoCluster l -- geometric cluster corresponding to inductive one
  rg = induGeoCluster r
  lgi = geoInduCluster lg -- normalised versions of l,r (with standard assignment)
  rgi = geoInduCluster rg
  llhs = induGeoCluster (lhsass z lgi) -- map rule symbols in assignments to their lhss
  rlhs = induGeoCluster (lhsass z rgi) -- and then compute the geometric cluster
  ulhs = geoClusterLub llhs rlhs -- take their least upper bound
  lwit = geoInduWitness (GeoWitness (clspos llhs) (clstrm llhs) (clspos ulhs)) -- and inductive witnesses 
  rwit = geoInduWitness (GeoWitness (clspos rlhs) (clstrm rlhs) (clspos ulhs)) -- for being upper bound
  i = indexList (\s->not (isVar (trmHead s))) (trmArgs (skeleton (clsrgt lwit))) -- index of argument to decompose at
  ls = skeleton (clsrgt lwit)
  rs = skeleton (clsrgt rwit)
  lwittop = putAt ls (Fun v []) [i] -- decompose the witnesses accordingly  
  lwitbot = trmAt ls [i]  
  rwittop = putAt rs (Fun v []) [i]
  rwitbot = trmAt rs [i]
  v = genvar (varAwayFrom (varsList (src z l))) -- generate a variable not occurring in the source
  glgi = gapass lgi  -- and then apply the substitutions witnessing refinement to the components
  grgi = gapass rgi
  lwitwit = witness lwit
  rwitwit = witness rwit
  ltop = (InduCluster (gassTrm lwitwit lwittop) glgi) 
  rtop = (InduCluster (gassTrm rwitwit rwittop) grgi) 
  lbot = (InduCluster (gassTrm lwitwit lwitbot) glgi) 
  rbot = (InduCluster (gassTrm rwitwit rwitbot) grgi) -- previously mistakenly had put glgi (copy-paste...)
lft (x,_,_) = x -- triple projections
mid (_,x,_) = x -- useful when we have triples
rgt (_,_,x) = x
-- compose si <-o- ti -o-> ui for i=1,2 as s1[v:=s2] <-o- t1[v:=t2] -o-> u1[v:=u2]
lpeakCompose :: Signature a => LocalPeak a -> a -> LocalPeak a -> LocalPeak a
lpeakCompose (LocalPeak z lt rt) v (LocalPeak _ lb rb) = LocalPeak z (clsSaferCompose lt [(v,lb)]) (clsSaferCompose rt [(v,rb)])
-- to test whether composing after decomposing is the identity
lpeakRecompose  ::  Signature a => LocalPeak a -> LocalPeak a
lpeakRecompose p = case (lpeakDecompose p) of
  (t,v,b) -> lpeakCompose t v b

-- p11
-- Section 5
-- first we illustrate the general idea (of the recursion) for orthogonal systems,
-- computing a local valley from a local peak of multisteps
data LocalValley a = LocalValley {
  lvtrs :: (TRS a),
  lvmstp :: (InduCluster a),
  rvmstp :: (InduCluster a)
}
instance Signature a => Show (LocalValley a) where
   show (LocalValley z c d) = (show (Multistep True True z c))++(show (Multistep False False z d))
lValleyCompose :: Signature a => LocalValley a -> a -> LocalValley a -> LocalValley a
lValleyCompose (LocalValley z lt rt) v (LocalValley w lb rb) = LocalValley w (clsCompose lt [(v,lb')]) (clsCompose rt [(v,rb')]) where
  lb' = standardiseInduCluster (maxGapIndex (symInduCluster lt)) lb
  rb' = standardiseInduCluster (maxGapIndex (symInduCluster rt)) rb
swapLV :: LocalValley a -> LocalValley a -- to deal with symmetry between outer--inner and inner--outer case
swapLV (LocalValley z l r) = (LocalValley z r l)
lValleyTrivial :: Signature a => TRS a -> Trm a -> LocalValley a -- construct trivial valley, i.e. two empty multisteps on a given term
lValleyTrivial z t = LocalValley z c c where c = InduCluster t []

orthoDiamond :: Signature a => LocalPeak a -> LocalValley a
orthoDiamond p@(LocalPeak z l r) = if (lpeakSize p) <= 1 then emptyorcritical else recurse where
  emptyorcritical = if (lpeakCritical p) then critical else empty where
    critical = (LocalValley z u u) where
      u = InduCluster (tgt z l) []
    empty = (LocalValley z r' l') where
      r' = if (isGap (trmHead (skeleton l))) then InduCluster (tgt z l) [] else r
      l' = if (isGap (trmHead (skeleton r))) then InduCluster (tgt z r) [] else l 
  recurse = aux (lpeakDecompose p) where
    aux (t,v,b) = lValleyCompose v1 v v2 where
      v1 = orthoDiamond t
      v2 = orthoDiamond b
      
-- some example peaks in the ortho trs ctrs, p(x) -> f(x,x)
cStp = InduCluster (symGapa[vara 2]) [(asymGap,rulonea[vara 1])]
dStp = InduCluster (symprda[symGapa[symprda[symzera]]]) [(asymGap,rulonea[vara 1])]
bPeak = LocalPeak ctrs cStp cStp
cPeak = LocalPeak ctrs cStp dStp
dPeak = LocalPeak ctrs dStp dStp
ePeak = LocalPeak ctrs aStp cStp
fPeak = LocalPeak ctrs bStp dStp
eStp = InduCluster (symsuca[symGapa[symprda[vara 2]]]) [(asymGap,rulonea[vara 1])]
fStp = InduCluster (symGapa[symGapb[vara 2]]) [(asymGap,ruloneb[vara 1]),(bsymGap,ruloneb[vara 1])]
-- fStp is ( X(Y(v2)) | [(X,θ(v1)),(Y,θ(v1))] )
-- eStp is ( s(X(p(v2))) | [(X,ρ(v1))] )
-- induInnerOverlapPairs  ((lhsass btrs eStp),(lhsass btrs fStp)) is ((X,Y),LT)

data DevClosure a = DevClosure {
    dctrs :: (TRS a),
    devclosures :: PfunGraph (LocalPeak a) (InduCluster a)
}
instance Signature a => Show (DevClosure a) where
  show (DevClosure z l) = show(z)++"(OUTER-INNER DEVELOPMENT CLOSURES\n"++(concat (map (\d->(show (fst d))++" by "++(show(Multistep False True z (snd d))++"\n")) l))++")\n"
gPeak = (LocalPeak btrs -- critical peak
      (InduCluster (symGapa[symprda[vara 1]]) ([(asymGap,rulonea[vara 1])]))
      (InduCluster (symprda[symGapa[vara 1]]) ([(asymGap,ruloneb[vara 1])])))
gPeak' = (LocalPeak btrs
      (InduCluster (symGapa[symprda[vara 2]]) ([(asymGap,rulonea[vara 1])]))
      (InduCluster (symprda[symGapa[vara 2]]) ([(asymGap,ruloneb[vara 1])])))
gPeak'' = (LocalPeak btrs
      (InduCluster (symprda[symGapa[vara 2]]) ([(asymGap,ruloneb[vara 1])]))
      (InduCluster (symGapa[symprda[vara 2]]) ([(asymGap,rulonea[vara 1])])))
hPeak = (LocalPeak btrs -- critical peak
      (InduCluster (symGapa[symsuca[vara 1]]) ([(asymGap,ruloneb[vara 1])]))
      (InduCluster (symsuca[symGapa[vara 1]]) ([(asymGap,rulonea[vara 1])])))
gPeak''' = (LocalPeak btrs
      (InduCluster (symprda[symprda[symGapa[vara 2]]]) ([(asymGap,ruloneb[vara 1])]))
      (InduCluster (symprda[symGapa[symprda[vara 2]]]) ([(asymGap,rulonea[vara 1])])))
iPeak = (LocalPeak btrs
       (InduCluster (symzera) ([]))
       (InduCluster (symzera) ([])))
jPeak = (LocalPeak btrs
       (InduCluster (symprda[symsuca[symzera]]) ([]))
       (InduCluster (symGapa[symzera]) ([(asymGap,rulonea[vara 1])])))
jPeak' = (LocalPeak btrs
       (InduCluster (symprda[symprda[symsuca[symzera]]]) ([]))
       (InduCluster (symprda[symGapa[symzera]]) ([(asymGap,rulonea[vara 1])])))
runlMStep = (InduCluster (symGapa[symprda[symGapb[symsuca[vara 2]]]]) ([(asymGap,rulonea[vara 1]),(bsymGap,ruloneb[vara 1])]))
runrMStep = (InduCluster (symprda[symsuca[symGapa[symGapb[vara 2]]]]) ([(asymGap,rulonea[vara 1]),(bsymGap,rulonea[vara 1])]))
runlMStep' = (InduCluster (symGapa[symprda[symsuca[symprda[symsuca[vara 2]]]]]) ([(asymGap,rulonea[vara 1])]))
runPeak = (LocalPeak btrs
          runlMStep
          runrMStep)
runPeak' = (LocalPeak btrs
            runlMStep'
            runrMStep)
btrsdev :: DevClosure Siga
btrsdev = DevClosure btrs
  [(gPeak,(InduCluster (symprda[vara 1]) ([]))),
   (hPeak,(InduCluster (symsuca[vara 1]) ([])))]
kPeak = (LocalPeak dtrs
         (InduCluster symGapc ([(csymGap,rulzera)]))
         (InduCluster symGapc ([(csymGap,rulzerb)])))
lPeak = (LocalPeak dtrs
         (InduCluster symGapc ([(csymGap,rulzerb)]))
         (InduCluster symGapc ([(csymGap,rulzera)])))
mPeak = (LocalPeak dtrs
         (InduCluster symGapc ([(csymGap,rulzera)]))
         (InduCluster symzeraa ([])))
nPeak = (LocalPeak dtrs
          (InduCluster (symbina[symGapc,symzera]) ([(csymGap,rulzera)]))
          (InduCluster (symbina[symGapc,symzera]) ([(csymGap,rulzerb)])))
oPeak = (LocalPeak dtrs
          (InduCluster (symbina[symGapc,symzera]) ([(csymGap,rulzera)]))
          (InduCluster (symbina[symGapc,symzera]) ([(csymGap,rulzera)])))
dtrsdev = DevClosure dtrs
  [(kPeak,(InduCluster symGapc ([(csymGap,rulzerd)]))),
   (lPeak,(InduCluster symGapc ([(csymGap,rulzerc)])))]
normaliseDClosure :: Signature a => DevClosure a -> DevClosure a
normaliseDClosure (DevClosure z l) = (DevClosure z (map aux l)) where
  aux ((LocalPeak _ c d),e) = ((LocalPeak z (bb c) (bb d)),bb e)
closure :: Signature a => DevClosure a -> LocalPeak a -> InduCluster a -- find closure for a given critical peak
closure d p = case (graphPfun (devclosures (normaliseDClosure d)) p) of
  Just c -> c
devclosedDiamond :: Signature a => DevClosure a -> LocalPeak a -> LocalValley a
devclosedDiamond d (LocalPeak z bl br) = if (lpeakSize p) <= 1 then emptyorcritical else recurse where
  l = bb bl -- normalise clusters
  r = bb br
  p = (LocalPeak z l r)
  emptyorcritical = if (lpeakCritical p) then (if (lpeakTrivial p) then (lValleyTrivial z (tgt z (lmstp p))) else critical) else empty where
    -- handle critical inner--outer case by symmetry/swapping (first input peak, finally output valley)
    critical = if (snd f) == GT then (swapLV (aux (LocalPeak z r l) (snd (fst f),fst (fst f)))) else aux p (fst f) where
      f = (induInnerOverlapPairs ((lhsass z l),(lhsass z r))) -- find an innermost overlap pair and how its ordered
      aux p'@(LocalPeak z' pHi pSi) f' = devclosedDiamond d (LocalPeak z med pSi')  where
        outer = fst f' -- the `gaps having overlap', with outer corresponding to phi, and inner (or overlay) to psi
        inner = snd f'  -- i.e. in Phi = M[X1,..,Xn:=r1,..,rn] and Psi = N[Y1,..,Ym:=s1,..,sn] then some inner pair Xi,Yj 
        phi = induced z outer pHi -- phi
        pHi' = bb (coinduced z outer pHi) -- Phi' (normalisation not needed really since not below phi per choice of phi)
        psi = induced z inner pSi -- psi
        pSi' = bb (coinduced z inner pSi) -- Psi' 
        patphi = induGeoCluster (lhsass z phi) -- geometric pattern of lhs of phi
        patpsi = induGeoCluster (lhsass z psi) -- geometric pattern of lhs of psi
        patu = geoClusterLub patphi patpsi -- union u of patterns of phi and psi
        lwit = geoInduWitness (GeoWitness (clspos patphi) (clstrm patphi) (clspos patu)) -- witnesses to (pat of) phi <= u
        rwit = geoInduWitness (GeoWitness (clspos patpsi) (clstrm patpsi) (clspos patu)) -- witnesses to (pat of) psi <= u
        cphi = InduCluster (snd(head(witness lwit))) [(fst(head(gapass(clslft lwit))),snd(head(gapass phi)))]-- critical encomp of phi
        cpsi = InduCluster (snd(head(witness rwit))) [(fst(head(gapass(clslft rwit))),snd(head(gapass psi)))]-- critical encomp of psi
        dev = closure d (LocalPeak z cphi cpsi) -- closing development for critical peak between outer phi and inner psi
        patpHi = induGeoCluster (lhsass z pHi) -- geometric patterns of Phi
        patU = geoClusterLub patpHi patpsi -- union U of patterns of Phi and psi
        lWit = geoInduWitness (GeoWitness (clspos patpHi) (clstrm patpHi) (clspos patU)) -- witnesses to (pat of) pHi <= U
        rWit = geoInduWitness (GeoWitness (clspos patpsi) (clstrm patpsi) (clspos patU)) -- witnesses to (pat of) psi <= U
        med = bb(clsSaferCompose pHihat devass) -- mediating multistep as composed of pHi' and the closing development
        s = (skeleton (clsrgt lWit)) -- skeleton of U serves as skeleton for both
        hole = head [x | (x,y) <- witness lWit, y == (skeleton cphi)] -- find hole of U to compose on     
        assnotHole = Prelude.filter (\(x,y) -> not (x == hole)) (witness lWit) -- remainder of assignment
        pHihatass = map (\(x,y) -> (x,g (graphPfun (gapass pHi) (trmHead y)))) assnotHole 
        g w = case w of
          Just v -> v
        -- standardise phihat wrt dev in order to avoid clashes between both, i.e. on the domain of the gaps
        -- pHihat = standardiseInduCluster (max (maxGapIndex (symInduCluster dev)) (gapindex hole)) (InduCluster s pHihatass)
        -- now above replaced by doing this in the safe composition when building med
        pHihat = (InduCluster s pHihatass)
        devass = [(hole,dev)]
    empty = case (lpeakEmpty p) of
      True -> (LocalValley z r' l') where
        r' = if (isGap (trmHead (skeleton l))) then InduCluster (tgt z l) [] else r
        l' = if (isGap (trmHead (skeleton r))) then InduCluster (tgt z r) [] else l   
  recurse = aux' (lpeakDecompose p) where
    aux' (t,v,b) = lValleyCompose v1 v v2 where
      v1 = devclosedDiamond d t
      v2 = devclosedDiamond d b
      
data SemiValley a = SemiValley {
  svtrs :: (TRS a),
  svmred :: [InduCluster a],
  svmstp :: (InduCluster a)
}
instance Signature a => Show (SemiValley a) where
   show (SemiValley z c d) = (show (Reduction True True z i c))++(show (Multistep False False z d)) where
     i = if (c == []) then (tgt z d) else (src z (head c)) -- if reduction is empty, take the target of the multistep
data SemiClosure a = SemiClosure {
    sctrs :: (TRS a),
    semiclosures :: PfunGraph (LocalPeak a) (SemiValley a)
}
instance Signature a => Show (SemiClosure a) where
  show (SemiClosure z l) = show(z)++"(MULTI-ONE CLOSURES\n"++(concat (map (\d->(show (fst d))++" by \n"++(show(snd d)++"\n")) l))++")\n"
etrs :: TRS Siga
etrs = TRS [(arulthr,(symbina[vara 1,symbina[vara 2,vara 3]],symbina[symbina[vara 1,vara 2],vara 3])),
            (brultwo,(symbina[vara 1,vara 2],symbina[vara 2,vara 1]))]
peak1 = LocalPeak etrs
         (InduCluster (symGap12a[vara 1,symbina[vara 2,vara 3]]) ([(symGap12,rultwob[vara 1,vara 2])]))
         (InduCluster (symGap13a[vara 1,vara 2,vara 3]) ([(symGap13,rulthra[vara 1,vara 2,vara 3])]))
reduction1 = [(InduCluster (symGap12a[symbina[vara 2,vara 3],vara 1]) ([(symGap12,rultwob[vara 1,vara 2])])),
              (InduCluster (symGap13a[vara 1,vara 2,vara 3]) ([(symGap13,rulthra[vara 1,vara 2,vara 3])]))]
multi1 = (InduCluster (symbina[symbina[vara 1,vara 2],vara 3]) [])
semi1 = SemiValley etrs reduction1 multi1 
etrssemi = SemiClosure etrs
  [(peak1,semi1)]
normaliseSClosure :: Signature a => SemiClosure a -> SemiClosure a
normaliseSClosure (SemiClosure z l) = (SemiClosure z (map aux l)) where
  aux ((LocalPeak _ c d),(SemiValley z l r)) = ((LocalPeak z (bb c) (bb d)),(SemiValley z (map bb l) (bb r)))
sclosure :: Signature a => SemiClosure a -> LocalPeak a -> SemiValley a -- find closure for a given critical peak
sclosure d p = case (graphPfun (semiclosures (normaliseSClosure d)) p) of
  Just c -> c

-- t[v:=R] where R is a (non-empty) sequence of steps (forming a reduction)
reductioniCompose :: Signature a => Trm a -> a -> [InduCluster a] -> [InduCluster a]
reductioniCompose t v [] = [] 
reductioniCompose t v (h:r) = (clsSaferCompose (InduCluster t []) [(v,h)]):(reductioniCompose t v r)
-- R[v:=t] where R is as above
reductionoCompose :: Signature a => [InduCluster a] -> a -> Trm a -> [InduCluster a]
reductionoCompose [] v t = [] 
reductionoCompose (h:r) v t = (clsSaferCompose h [(v,(InduCluster t []))]):(reductionoCompose r v t)
-- R[v:=S] with R,S as above, as composition (src R)[v:=S];R[v:=tgt S] 
reductionCompose :: Signature a => TRS a -> [InduCluster a] -> a -> [InduCluster a] -> [InduCluster a]
reductionCompose z r v s = (reductioniCompose (src z (head r)) v s)++(reductionoCompose r v (tgt z (last s)))
-- compose two semi-valleys by composing their respectiv reductions (made non-empty if necessary) and multisteps, componentwise
sValleyCompose :: Signature a => SemiValley a -> a -> SemiValley a -> SemiValley a
sValleyCompose (SemiValley z lt rt) v (SemiValley w lb rb) = SemiValley w (reductionCompose z lt' v lb') (clsSaferCompose rt [(v,rb)]) where
  lt' = if (lt == []) then [InduCluster (tgt z rt) []] else lt
  lb' = if (lb == []) then [InduCluster (tgt z rb) []] else lb
sValleyTrivial :: Signature a => TRS a -> Trm a -> SemiValley a -- construct trivial valley, i.e. two empty reduction and multistep on a given term
sValleyTrivial z t = SemiValley z [] c where c = InduCluster t []

-- decompose a term of shape f(vk1,...,vkn) into one of shape f(v1,...,v) and assignment vi := vki
-- doesn't check for shape
varDecompose :: Signature a => Trm a -> (Trm a,PfunGraphTrm a)
varDecompose t = (t',g') where
  t' = Fun h (map vara [1..(arity h)])
  h = trmHead t
  vs = nvars (arity h)
  g' = zip vs (trmArgs t)
-- varDecompose (symbina[vara 5,vara 2]) is (f(v1,v2),[(v1,v5),(v2,v2)])
-- recompose to test decomposition
varRecompose :: Signature a => Trm a -> Trm a
varRecompose t = case (varDecompose t) of
  (t',g) -> gassTrm g t'
-- ok, varRecompose (symbina[vara 5,vara 2]) is f(v5,v2) which is symbina[vara 5,vara 2]
-- extend to clusters and peaks
varCDecompose :: Signature a => InduCluster a -> (InduCluster a,PfunGraphTrm a)
varCDecompose (InduCluster s g) = (c',g') where
  c' = InduCluster (fst d) g
  g' = snd d
  d = varDecompose s
-- decompose a variable instance of critical local peak, in the critical local peak and instantiation
-- we assume the former is known to be the case
varLPeakDecompose :: Signature a => LocalPeak a -> (LocalPeak a,PfunGraphTrm a)
varLPeakDecompose (LocalPeak z l r) = (LocalPeak z cl cr,g) where
  patl = induGeoCluster (lhsass z l) -- geometric pattern of lhs of l
  patr = induGeoCluster (lhsass z r) -- geometric pattern of rhs of r
  patu = geoClusterLub patl patr -- union of patterns of lhss of l and r (by assumption this yields a cluster of shape X(vs)[X:=t]
  lwit = geoInduWitness (GeoWitness (clspos patl) (clstrm patl) (clspos patu)) -- linearised skeleton of l is witness to inclusion
  rwit = geoInduWitness (GeoWitness (clspos patr) (clstrm patr) (clspos patu)) -- linearised skeleton of r is witness to inclusion
  cl = InduCluster (snd(head(witness lwit))) (gapass l) -- retrofit original rules in l to its linearised skeleton
  cr = InduCluster (snd(head(witness rwit))) (gapass r) -- retrofit original rules in r to its linearised skeleton
  g = snd (varDecompose (skeleton (geoInduCluster patu)))
-- varLPeakDecompose bPeak is (f(v1,v1) π(v1)<-- p(v1) -->π(v1) f(v1,v1),[(v1,v2)])
-- for bPeak being f(v2,v2) π(v2)<-- p(v2) -->π(v2) f(v2,v2)

-- apply a var substitition to all skeletons of clusters in a valley
varSValleyCompose  :: Signature a => SemiValley a -> PfunGraphTrm a -> SemiValley a
varSValleyCompose (SemiValley z r c) g = SemiValley z (map f r) (f c) where
  f (InduCluster s h) = InduCluster (gassTrm g s) h 

-- Okui's result that if all multi--one critical peaks can be closed as -o->*;<-o- then so can all multi--one peaks
okuiMultiOne :: Signature a => SemiClosure a -> LocalPeak a -> SemiValley a -- assumes right step of local peak contains at most one step
okuiMultiOne d (LocalPeak z dl dr) = if (lpeakSize p) <= 1 then emptyorcritical else recurse where
  p = LocalPeak z l r
  l = bb dl -- normalise input
  r = bb dr
  emptyorcritical = if (lpeakCritical p) then (if (lpeakTrivial p) then (sValleyTrivial z (tgt z (lmstp p))) else critical) else empty where
    critical = varSValleyCompose (sclosure d (fst dp)) (snd dp) where -- search for -o->*;<-o- closure in list of closures, solve, and var inst
      dp = varLPeakDecompose p -- decomposition into critical peak and variable instantiation
    empty = (SemiValley z [r'] l') where
      r' = if (isGap (trmHead (skeleton l))) then InduCluster (tgt z l) [] else r
      l' = if (isGap (trmHead (skeleton r))) then InduCluster (tgt z r) [] else l 
  recurse = aux (lpeakDecompose p) where
    aux (t,v,b) = sValleyCompose v1 v v2 where
      v1 = okuiMultiOne d t
      v2 = okuiMultiOne d b

abstractcls = (InduCluster (symprda[symGapa[symzera]]) ([(asymGap,symprda[symsuca[vara 1]])]))
-- orthoDiamond fPeak

-- to be extended