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