TYPE 
  Text = Nr -> Line;
  Line = Nr -> Char;
  Char = STR;   
  Nr = INT;
  Cursor :: L:Nr
            C: Nr;
  EdSt   :: C:Cursor
            T:Text;
ENDTYPE

FUNC  InvEdSt () : 
RETURNS  let ( c = C(S),
               t = T(S),
               y = L(c),
               x = C(c) )
          in  SequenceStruct(t) /\ CursorLimits(x,y,t);

SequenceStruct(t) =  IsSequence(t) /\ all(l <- dom(t) : IsSequence(t[l]));

IsSequence(f) = ( dom(f) == inseg(card(dom(f))) );

CursorLimits(x,y,t) =  y <= len(t) /\  x <= len(t[y]);
 

FUNC Init() :
STATE  S <- EdSt(Cursor(0,0),[]);

FUNC  G (n:Nr) :
PRE   n <= len(T(S))
STATE S <- EdSt(Cursor(n,1), T(S));

FUNC  r (c:Char) :
PRE   T(S) != []
STATE  let ( x = C(C(S)),
             y = L(C(S)),
             t = T(S),
             l = t[y],
             nl = l + [x -> c] )
        in  S <- EdSt(C(S), t + [y -> nl]);


FUNC dd (n:Nr) :
STATE  let ( c = C(S),
             t = T(S),
             c1 = newCur(c,t,n),
             t1 = remove(t,L(c),n) )
       in  S <- EdSt(c1,t1);

newCur(c,t,n) = if ( (len(t) .- n) >= L(c) )
                then c
                else (if ( len(t[(L(c) .- 1)]) < C(c) )
                      then (if L(c) == 1 
                            then Cursor(0,0)
                            else Cursor(( L(c) .- 1),len(t[(L(c) .- 1)])))
                       else Cursor(( L(c) .- 1), C(c)));

remove(s,m,n) = s/inseg(m .- 1) + shift(s\inseg(n .+ m .- 1),n);

shift(s,n) = [i  -> s[(i .+ n)] | i <- subn(n,dom(s))];

subn(n,s) = {i .- n | i <- s};

len(s) = card(dom(s));



S <-
EdSt(Cursor(3,3),[1 -> [1 ->"a", 2->"b",3->"c",4->"d"],
2 -> [1 ->"a2"],
3 -> [1 ->"a3",2->"b3",3->"c3"],
4 -> [1->"a4",2->"b4",3->"c4"]]);
P <-
EdSt(Cursor(2,2),[1 -> [1 ->"a", 2->"b",3->"c",4->"d"],
2 -> [1 ->"a2",2->"b2",3->"c2"],
3 -> [1 ->"a3",2->"b3",3->"c3"],
4 -> [1->"a4",2->"b4",3->"c4"]]);
Y <-
EdSt(Cursor(2,5),[1 -> [1 ->"a", 2->"b",3->"c"],
2 -> [1 ->"a1",2->"b1",3->"c1"],
3 -> [1->"a2",2->"b2",3->"c2"]]);