spec BooleanAlgebra = sort Elem ops 0 : Elem; 1 : Elem; __cap__ : Elem*Elem->Elem; __cup__ : Elem*Elem->Elem end spec EquivalenceRelation = sort Elem pred __~__ : Elem*Elem end spec ExtBooleanAlgebra %% [...] %% = sort Elem ops 0 : Elem; 1 : Elem; __cap__ : Elem*Elem->Elem; __cup__ : Elem*Elem->Elem; compl : Elem->Elem preds __<=__ : Elem*Elem; __<__ : Elem*Elem; __>=__ : Elem*Elem; __>__ : Elem*Elem end spec ExtPartialOrder %% [...] %% = sort Elem ops inf : Elem*Elem->?Elem; sup : Elem*Elem->?Elem preds __<=__ : Elem*Elem; __<__ : Elem*Elem; __>=__ : Elem*Elem; __>__ : Elem*Elem end spec ExtTotalOrder %% [...] %% = sort Elem ops inf : Elem*Elem->?Elem; max : Elem*Elem->Elem; min : Elem*Elem->Elem; sup : Elem*Elem->?Elem preds __<=__ : Elem*Elem; __<__ : Elem*Elem; __>=__ : Elem*Elem; __>__ : Elem*Elem end spec Int = sorts Nat,Pos < Int; Pos < Nat; Pos ops +__ : Nat->Nat; +__ : Int->Int; -__ : Nat->Int; -__ : Int->Int; 0 : Nat; 0 : Int; 1 : Nat; 1 : Pos; 1 : Int; 2 : Nat; 3 : Nat; 4 : Nat; 5 : Nat; 6 : Nat; 7 : Nat; 8 : Nat; 9 : Nat; Nat : Int; __! : Nat->Nat; __*__ : Nat*Nat->Nat; __*__ : Pos*Pos->Pos; __*__ : Int*Int->Int; __+__ : Nat*Nat->Nat; __+__ : Nat*Pos->Pos; __+__ : Pos*Nat->Pos; __+__ : Int*Int->Int; __-?__ : Nat*Nat->?Nat; __-__ : Nat*Nat->Int; __-__ : Int*Int->Int; __/?__ : Nat*Nat->?Nat; __/?__ : Int*Int->?Int; __@@__ : Nat*Nat->Nat; __^__ : Nat*Nat->Nat; __^__ : Int*Nat->Int; __div__ : Nat*Nat->?Nat; __div__ : Int*Int->?Int; __mod__ : Nat*Nat->?Nat; __mod__ : Int*Int->?Nat; __quot__ : Nat*Nat->?Nat; __quot__ : Int*Int->?Int; __rem__ : Nat*Nat->?Nat; __rem__ : Int*Int->?Int; abs : Nat->Nat; abs : Int->Nat; max : Nat*Nat->Nat; max : Int*Int->Int; min : Nat*Nat->Nat; min : Int*Int->Int; pre : Nat->?Nat; sign : Int->Int; suc : Nat->Nat; suc : Nat->Pos preds __<=__ : Nat*Nat; __<=__ : Int*Int; __<__ : Nat*Nat; __<__ : Int*Int; __>=__ : Nat*Nat; __>=__ : Int*Int; __>__ : Nat*Nat; __>__ : Int*Int; even : Nat; even : Int; odd : Nat; odd : Int end spec Nat = sorts Pos < Nat; Pos ops +__ : Nat->Nat; 0 : Nat; 1 : Nat; 1 : Pos; 2 : Nat; 3 : Nat; 4 : Nat; 5 : Nat; 6 : Nat; 7 : Nat; 8 : Nat; 9 : Nat; __! : Nat->Nat; __*__ : Nat*Nat->Nat; __*__ : Pos*Pos->Pos; __+__ : Nat*Nat->Nat; __+__ : Nat*Pos->Pos; __+__ : Pos*Nat->Pos; __-?__ : Nat*Nat->?Nat; __/?__ : Nat*Nat->?Nat; __@@__ : Nat*Nat->Nat; __^__ : Nat*Nat->Nat; __div__ : Nat*Nat->?Nat; __mod__ : Nat*Nat->?Nat; __quot__ : Nat*Nat->?Nat; __rem__ : Nat*Nat->?Nat; abs : Nat->Nat; max : Nat*Nat->Nat; min : Nat*Nat->Nat; pre : Nat->?Nat; suc : Nat->Nat; suc : Nat->Pos preds __<=__ : Nat*Nat; __<__ : Nat*Nat; __>=__ : Nat*Nat; __>__ : Nat*Nat; even : Nat; odd : Nat end spec PartialEquivalenceRelation = sort Elem pred __~__ : Elem*Elem end spec PartialOrder = sort Elem pred __<=__ : Elem*Elem end %[ view PartialOrder_in_ExtBooleanAlgebra = end ]% spec PreOrder = sort Elem pred __<=__ : Elem*Elem end spec Rat = sorts Nat,Pos < Int; Pos < Nat; Pos; Int,Nat,Pos < Rat ops +__ : Nat->Nat; +__ : Int->Int; +__ : Rat->Rat; -__ : Nat->Int; -__ : Int->Int; -__ : Rat->Rat; 0 : Nat; 0 : Int; 0 : Rat; 1 : Nat; 1 : Pos; 1 : Int; 1 : Rat; 2 : Nat; 3 : Nat; 4 : Nat; 5 : Nat; 6 : Nat; 7 : Nat; 8 : Nat; 9 : Nat; Nat : Int; __! : Nat->Nat; __*__ : Nat*Nat->Nat; __*__ : Pos*Pos->Pos; __*__ : Int*Int->Int; __*__ : Rat*Rat->Rat; __+__ : Nat*Nat->Nat; __+__ : Nat*Pos->Pos; __+__ : Pos*Nat->Pos; __+__ : Int*Int->Int; __+__ : Rat*Rat->Rat; __-?__ : Nat*Nat->?Nat; __-__ : Nat*Nat->Int; __-__ : Int*Int->Int; __-__ : Rat*Rat->Rat; __/?__ : Nat*Nat->?Nat; __/?__ : Int*Int->?Int; __/__ : Int*Pos->Rat; __/__ : Rat*Rat->?Rat; __@@__ : Nat*Nat->Nat; __^__ : Nat*Nat->Nat; __^__ : Int*Nat->Int; __^__ : Rat*Int->Rat; __div__ : Nat*Nat->?Nat; __div__ : Int*Int->?Int; __mod__ : Nat*Nat->?Nat; __mod__ : Int*Int->?Nat; __quot__ : Nat*Nat->?Nat; __quot__ : Int*Int->?Int; __rem__ : Nat*Nat->?Nat; __rem__ : Int*Int->?Int; abs : Nat->Nat; abs : Int->Nat; abs : Rat->Rat; max : Nat*Nat->Nat; max : Int*Int->Int; max : Rat*Rat->Rat; min : Nat*Nat->Nat; min : Int*Int->Int; min : Rat*Rat->Rat; pre : Nat->?Nat; sign : Int->Int; suc : Nat->Nat; suc : Nat->Pos preds __<=__ : Nat*Nat; __<=__ : Int*Int; __<=__ : Rat*Rat; __<__ : Nat*Nat; __<__ : Int*Int; __<__ : Rat*Rat; __>=__ : Nat*Nat; __>=__ : Int*Int; __>=__ : Rat*Rat; __>__ : Nat*Nat; __>__ : Int*Int; __>__ : Rat*Rat; even : Nat; even : Int; odd : Nat; odd : Int end spec ReflexiveRelation = sort Elem pred __~__ : Elem*Elem end spec Relation = sort Elem pred __~__ : Elem*Elem end spec RichBooleanAlgebra = sort Elem ops 0 : Elem; 1 : Elem; __cap__ : Elem*Elem->Elem; __cup__ : Elem*Elem->Elem; compl : Elem->Elem preds __<=__ : Elem*Elem; __<__ : Elem*Elem; __>=__ : Elem*Elem; __>__ : Elem*Elem end spec RichPartialOrder = sort Elem ops inf : Elem*Elem->?Elem; sup : Elem*Elem->?Elem preds __<=__ : Elem*Elem; __<__ : Elem*Elem; __>=__ : Elem*Elem; __>__ : Elem*Elem end spec RichTotalOrder = sort Elem ops inf : Elem*Elem->?Elem; max : Elem*Elem->Elem; min : Elem*Elem->Elem; sup : Elem*Elem->?Elem preds __<=__ : Elem*Elem; __<__ : Elem*Elem; __>=__ : Elem*Elem; __>__ : Elem*Elem end spec SigOrder %% [...] %% = sort Elem preds __<=__ : Elem*Elem; __<__ : Elem*Elem; __>=__ : Elem*Elem; __>__ : Elem*Elem end spec SimilarityRelation = sort Elem pred __~__ : Elem*Elem end spec SymmetricRelation = sort Elem pred __~__ : Elem*Elem end spec TotalOrder = sort Elem pred __<=__ : Elem*Elem end %[ view TotalOrder_in_Int = sorts Elem |-> Int end ]% %[ view TotalOrder_in_Nat = sorts Elem |-> Nat end ]% %[ view TotalOrder_in_Rat = sorts Elem |-> Rat end ]% spec TransitiveRelation = sort Elem pred __~__ : Elem*Elem end