ws1s; pred close(var1 x, var1 y, var2 M) = x close(c1,cn,M)) & (c+1=cn => close(c,cn,M)) & (p+1=c => close(p,c,M)) & (close(c1,cn1,M) => c1+1=cn1) & (close(p1,c1,M) => p1+1=c1) ); all1 end: ex1 c,cn,p,c1,cn1,p1,exdv1,exdv2 : ( validmodel(end,c,cn,p,c1,cn1,p1,exdv1,exdv2) & minimalmodel(end,c,cn,p,c1,cn1,p1,exdv1,exdv2) ) ;