fmod GILBREATH-ACU is
sorts Boolean Card List NeList .
subsort Card < NeList .
subsort NeList < List .
op False : -> Boolean [ ctor metadata "1" ] .
op True : -> Boolean [ ctor metadata "0" ] .
op __ : List List -> List [ assoc id: nil metadata "5" ] .
op __ : NeList NeList -> NeList [ assoc ctor id: nil metadata "5" ] .
op alter : List -> Boolean [ metadata "8" ] .
op black : -> Card [ ctor metadata "3" ] .
op even : List -> Boolean [ metadata "11" ] .
op neg : Card -> Card [ metadata "12" ] .
op nil : -> List [ ctor metadata "2" ] .
op opposite : List List -> Boolean [ metadata "7" ] .
op paired : Card Card -> Boolean [ metadata "6" ] .
op pairedList : List -> Boolean [ metadata "9" ] .
op red : -> Card [ ctor metadata "4" ] .
op rotate : List -> List [ metadata "13" ] .
op shuffle : List List List -> Boolean [ metadata "10" ] .
eq alter(C:Card) = True .
eq alter(nil) = True .
eq even(C:Card) = False .
eq even(nil) = True .
eq even(L1:List C1:Card L2:List C2:Card L3:List) = even(L1:List L2:List L3:List) .
eq neg(black) = red [ variant ] .
eq neg(red) = black [ variant ] .
eq opposite(L:List, nil) = False [ variant ] .
eq opposite(nil, L:List) = False [ variant ] .
eq opposite(C1:Card L1:List, C2:Card L2:List) = paired(C1:Card, C2:Card) [ variant ] .
eq paired(C:Card, C:Card) = False [ variant ] .
eq paired(black, red) = True [ variant ] .
eq paired(red, black) = True [ variant ] .
eq pairedList(C:Card) = False .
eq pairedList(nil) = True .
eq pairedList(C:Card C:Card L:List) = False .
eq rotate(nil) = nil [ variant ] .
eq rotate(C:Card L:List) = L:List C:Card [ variant ] .
eq shuffle(L1:List, C2:Card L2:List, nil) = False .
eq shuffle(nil, nil, nil) = True .
eq shuffle(nil, nil, C3:Card L3:List) = False .
eq shuffle(C1:Card L1:List, L2:List, nil) = False .
ceq alter(C1:Card C2:Card L:List) = False if paired(C1:Card, C2:Card) = False .
ceq alter(C1:Card C2:Card L:List) = alter(C2:Card L:List) if paired(C1:Card, C2:Card) = True .
ceq pairedList(C1:Card C2:Card L:List) = pairedList(L:List) if paired(C1:Card, C2:Card) = True .
ceq shuffle(nil, C2:Card L2:List, C3:Card L3:List) = False if paired(C2:Card, C3:Card) = True .
ceq shuffle(nil, C2:Card L2:List, C3:Card L3:List) = shuffle(nil, L2:List, L3:List) if paired(C2:Card, C3:Card) = False .
ceq shuffle(C1:Card L1:List, nil, C3:Card L3:List) = False if paired(C1:Card, C3:Card) = True .
ceq shuffle(C1:Card L1:List, nil, C3:Card L3:List) = shuffle(L1:List, nil, L3:List) if paired(C1:Card, C3:Card) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if paired(C1:Card, C3:Card) = True /\ paired(C2:Card, C3:Card) = True .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if paired(C1:Card, C3:Card) = True /\ shuffle(C1:Card L1:List, L2:List, L3:List) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if paired(C2:Card, C3:Card) = True /\ shuffle(L1:List, C2:Card L2:List, L3:List) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if shuffle(L1:List, C2:Card L2:List, L3:List) = False /\ shuffle(C1:Card L1:List, L2:List, L3:List) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = True if paired(C1:Card, C3:Card) = False /\ shuffle(L1:List, C2:Card L2:List, L3:List) = True .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = True if paired(C2:Card, C3:Card) = False /\ shuffle(C1:Card L1:List, L2:List, L3:List) = True .
endfm