re-create()∷ true
post-create(r)∷ ( [ ] , [ ] , [ ] , [ ] )

pre-destroy(t):: true
post-destroy(t; r):: r =  ⊥

pre-init(t) :: true
post-init∷ r = ( [ ] , [ ] , [ ] , [ ] )

pre-size(t)∷ true
post-size((l, q, h, b); r)∷ ( l ^^ q ^^ h )

pre-size(t):: true
post-size((l, q, h, b); r):: ( l ^^ q ^^ h ^^ b )

pre-cursorRight(t)∷ true
post-cursorRight(l, q, h, b); r):: r = ( l ^^ h ^^ [Head q], [ ], Tail q, b )

pre-cursorLeft(t)∷ true
post-cursorLeft((l, q, h, b); r):: r = ( l

pre-home(t)∷ true
post-home((l, q, h, b); r)∷ r = ( [ ] , l ^^ h ^^ q , [ ] , b )

pre-end(t)∷ true
post-end((l, q, h, b); r):: r = ( q ^^ h ^^ l, [ ] , [ ] , b )

pre-delete(t)∷ true
post-delete((l, q, h, b); r)∷ if h = [ ]
then
r = ( l, tail.q, [ ], b )
else
r = ( l, q, [], b )

pre-backspace(t)∷ true
post-backspace((l, q, h, b); r)∷ if h = [ ]
then
r = ( Reverse(Tail(Reverse(l), q , [ ], b )
else
r = ( l, q, [ ], b )

pre-highlightLeftCharacter∷ true
post-highlightLeftCharacter∷

pre-highlightRightCharacter∷ true
post-highlightRightCharacter∷

pre-highlightRightWord∷ true
post-highlightRightWord((l, q, h, b); r)∷ r = highlightRightWord(L, Q, H, B)
where
highlightRightWord(l, [ ], h, b) = (l, q, h, b)
hightlightRightWord(l, q, h, b) = if Head(q) = “ “ Then (l, q, h, b)
else
highlightRightWord(L, Tail(q), h ^^ [Head(q)], b)

pre-highlightLeftWord∷ true
post-highlightLeftWord((l, q, h, b);r)∷ r = highlightLeftWord(l, q, h, b)
where
highlightLeftWord(l, q, [ ], b) = (l, q, h, b)
highlightLeftWord(l, q, h, b) = if Head(q) = “ “ Then (l, q, h, b)
else
highlightLeftWord(l, Tail(q), h ^^ [Head(q)], b)

pre-copy(t)∷ true
post-copy((l, q, h, b)); r)∷ r = ( l , q , h ,  [ ] ^^ h )

pre-paste(t)∷ if totalSize(t) > 254
post-paste((l, q, h, b); r)∷ if h = [ ]
then
r = ( l, q ^^ b, [ ], b )
else
( l, q, [ ] ^^ b, b )

pre-cut(t)∷ true
post-cut((l, q, h, b); r)∷ r = ( l, q, [ ], [ ] ^^ h )

pre-selectAll(t)∷ true
post-selectAll((l, q, h, b); r)∷ r = ( l ^^ h ^^ q, b)

pre-deleteAll(t):: true
post-deleteAll((l, q, h, b); r):: r = ( [ ], [ ], [ ], b)

pre-addCharacter(t)∷ if size(t) > 254
post-addCharacter((l, q, h, b); r)∷

pre-skipWord(t):: true
post-skipWord(l, q, h, b); r)::

pre-backWord(t):: true
post-backWord(l, q, h, b); r)::