fmod IPS is
    protecting INT .
    
    sort IntStr .
    sort IPSTuple .
    sort IPSstr .

    op _(_) : IPSstr Int -> IPSTuple [prec 1] .
    op _(_) : IntStr Int -> Int [prec 1] .

    op U : -> Int .

    op _,_,_ : Int Int Int -> IPSTuple .
    op _,_,_ : IntStr IntStr IntStr -> IPSstr .

    op ips : IPSstr -> IPSstr .

    vars A B C : IntStr .
    var T : Int .
    
    eq ips(A,B,C)(0) = (U,U,U) .
    ***eq ips(A,B,C)(T + 1) = (A(T),B(T),
    ***                       A(T) * B(T) + C(T)) .
    eq ips(A,B,C)(T) = (A(T - 1),B(T - 1 ),
                        A(T - 1) * B(T - 1) + C(T - 1))
                      [owise] .
endfm

fmod IPS-RUN is
    protecting IPS .

    op a : -> IntStr .
    op b : -> IntStr .
    op c : -> IntStr .

    eq a(0) = 1 .
    eq a(1) = 2 .
    eq a(2) = 3 .
    
    eq b(0) = 4 .
    eq b(1) = 5 .
    eq b(2) = 6 .
    
    eq c(0) = 6 .
    eq c(1) = 7 .
    eq c(2) = 8 .
endfm

red ips(a,b,c)(0) .
red ips(a,b,c)(1) .
red ips(a,b,c)(2) .
red ips(a,b,c)(3) .