fmod SR is
    protecting INT .
    
    sorts IntStr BoolStr .
    
    op U : -> Int .
    
    op _(_) : IntStr Int -> Int .
    op _(_) : BoolStr Int -> Bool .
    
    op SR : IntStr BoolStr -> IntStr .

    op delta : BoolStr Int -> Int .
    op beenTrue : BoolStr Int -> Bool .

    var D : IntStr .
    var C : BoolStr .
    var T : Int .

    eq SR(D,C)(0) = U .
    ceq SR(D,C)(T) = U if not beenTrue(C,T - 1) and (T > 0) .
    ceq SR(D,C)(T) = D(delta(C,T - 1))
        if beenTrue(C,T - 1) and (T > 0) .

    eq beenTrue(C,0) = C(0) .
    ceq beenTrue(C,T) = true if (C(T) == true) and (T > 0) .
    ceq beenTrue(C,T) = beenTrue(C,T - 1)
        if (C(T) == false) and (T > 0) .

    ceq delta(C,0)= 0 if C(0) == true .
    ceq delta(C,T) = T if (C(T) == true) and (T > 0) .
    ceq delta(C,T) = delta(C, T - 1)
       if (C(T) == false) and (T > 0) .
endfm


fmod SR-RUN is
    protecting SR .
    
    op d : -> IntStr .
    op c : -> BoolStr .
    
    eq d(0) = 0 .
    eq d(1) = 1 .
    eq d(2) = 2 .
    eq d(3) = 3 .
    eq d(4) = 4 .
    
    eq c(0) = false .
    eq c(1) = false .
    eq c(2) = true .
    eq c(3) = false .
    eq c(4) = true .
endfm

red SR(d,c)(0) .
red SR(d,c)(1) .
red SR(d,c)(2) .
red SR(d,c)(3) .
red SR(d,c)(4) .
red SR(d,c)(5) .