-- Ja nao acredito no Pai Natal. So na Coelinha da Pascoa
types 

call = nat;

list_of_calls = seq of call
inv x == len(x) <= 10 and len(x) = card(elems(x))


functions

store1: list_of_calls * call -> list_of_calls
store1(lsc, call) == [call]^[ lsc(x) | x in set inds(lsc) & call <> lsc(x) and
        (if call in set elems(lsc) then x <= 10 else x <= 9)];

store2: list_of_calls * call -> list_of_calls
store2(lsc, call) == if ( call in set elems(lsc) ) 
        then [call]^[ lsc(x) | x in set inds(lsc) & call <> lsc(x) and x <= 10]
        else [call]^[ lsc(x) | x in set inds(lsc) & x <= 9 ];

store3: list_of_calls * call -> list_of_calls
store3(lsc, call) == let aux = [call]^[ lsc(i) | i in set inds lsc & lsc(i) <> call ]
                     in [ aux(i) | i in set inds aux & i <= 10 ]

types 

contingent  ::  operational : seq of nat
                resting : seq of nat
inv x == len( x.operational) > 0 and len( x.resting ) > 0

functions 

replacement1 : contingent -> contingent
replacement1(con) == let out = hd con.operational 
    in mk_contingent( (tl con.operational)^[hd con.resting], (tl con.resting)^[out]);

replacement2 : contingent -> contingent
replacement2(con) == let o = (tl con.operational) ^ [hd con.resting],
                         r = (tl con.resting) ^ [ hd con.operational ]
                     in mk_contingent(o, r)