load modules/succ.maude --- Line (1) is range [1,4] --- Line (2) is range [2,inf] --- Intersection is [2,4] red succ-mod : ({'s['X:Nat]} - {'s['s['s['s['s['X:Nat]]]]]}) & --- (1) {'s['s['X:Nat]]} --- (2) eq {'s['s['zero.Nat]]} U {'s['s['s['zero.Nat]]]} U {'s['s['s['s['zero.Nat]]]]} .