SequencesAsRelationsTest.mch

MACHINE SequencesAsRelationsTest
PROPERTIES
 {} = []
& {(1+0,1)} = [1]

/* Set of sequences */
& {(1+0,1)} : seq({1})
& {(1+0,2)} /: seq({1})
& not({(1+0,1)} /: seq({1}))
& {} : seq({1+0})
& {} : seq({})

& {x,y| x : 1..10 & y : {3}} : seq({3})
& {} \/ {} : seq({1})
& {x,y| x : 1..10 & y : {3}} : seq1({3})
& {} \/ {} /: seq1({1})


/* Set of sequences */
& {(1+0,1)} : seq1({1})
& {} /: seq1({})
& {(1+0,2)} /: seq1({1}) 
& not({} : seq1({1+0}))
& not({} : seq1({}))

/* Set of injective sequences */
& iseq({}) = {{}}
& iseq({1}) = {{},{(1+0,1)}}

/* Set of non empty injective sequences */
& iseq1({}) = {}
& iseq1({1}) = {{(1+0,1)}}

/* Size */
& size({}) = 0
& size({(1+0,1),(2,2)}) = 2

/* Concatenation */
& {(1+0,1),(2,2)}^{(1,3)} = {(1,1),(2,2),(3,3)}
& {(1+0,1),(2,2)}^{} = {(1,1),(2,2)}
& {}^{(1+0,1),(2,2)} = {(1,1),(2,2)}
& {}^{} = {}

/* Prepand */
& 1 -> {(1+0,2),(2,3)} = {(1,1),(2,2),(3,3)}
& 1 -> {} = {(1+0,1)}

/* Append */
& {(1+0,1),(2,2)} <- 3 = {(1,1),(2,2),(3,3)}
& {} <- 1 = {(1+0,1)}

/* Front */
& front({(1+0,1)}) = {}
& front({(1+0,1),(2,2),(3,3)}) = {(1,1),(2,2)}

/* First */
& first({(1+0,1)}) = 1
& first({(1+0,1),(2,2)}) = 1

/* Tail */
& tail({(1+0,1)}) = {}
& tail({(1+0,1),(2,2),(3,3)}) = {(1,2),(2,3)}

/* Last */
& last({(1+0,1)}) = 1
& last({(1+0,1),(2,2)}) = 2

/* Reverse */
& rev({}) = {}
& rev({(1+0,1)}) = {(1,1)}
& rev({(1+0,1),(2,2),(3,3)}) = {(1,3),(2,2),(3,1)}

/* Generalized Concatenation */
& conc({(1,{(1,1),(2,2)}),(2,{(1,3)})}) = {(1,1),(2,2),(3,3)}
& conc({(1,{(1,1),(2,2)}),(2,{})}) = {(1,1),(2,2)}
& conc({(1,{}), (2,{(1,1),(2,2)})}) = {(1,1),(2,2)}
& conc({(1,{}),(2,{})}) = {}
& conc([{}, {(1,1),(2,2)}]) =  {(1,1),(2,2)}

/* Perm */
& perm({3,4}) = {{(1,3),(2,4)},{(1,4),(2,3)}}
& perm({}) = {{}}

/* Take first elements */
& {(1+0,1),(2,2)} /|\ 1 = {(1,1)}
& {(1+0,1),(2,2)} /|\ 2 = {(1,1),(2,2)}
& {(1+0,1)} /|\ 0 = {}
& {} /|\ 0 = {}

& {(1+0,1),(2,2)} \|/ 1 = {(1,2)}
& {(1+0,1),(2,2)} \|/ 0 = {(1,1),(2,2)}
& {(1+0,1)} \|/ 1 = {}
& {} \|/ 0 = {}
END