ws1s; pred next(var1 x, var1 y, var1 nil, var1 end) = (x+1=y & y<=nil) | (nil<=y & y+1=x & x<=end) ; pred close(var1 x, var1 y, var2 M) = x next'(head,head1,nil,end,M)) & (before1(end,nil,head1,exdv1) => before1'(end,nil,head1,exdv1,M)) & (before1(end,nil,newhead1,exdv1) => before1'(end,nil,newhead1,exdv1,M)) & (before1(end,nil,exdv1,exdv2) => before1'(end,nil,exdv1,exdv2,M)) ); all1 end: ex1 nil,t,head,newhead,head1,newhead1,exdv1,exdv2 : ( validmodel(end,nil,t,head,newhead,head1,newhead1,exdv1,exdv2) & minimalmodel(end,nil,t,head,newhead,head1,newhead1,exdv1,exdv2) ) ;