ws1s; pred close(var1 x, var1 y, var2 M) = x close(curr,curr1,M)) & (prev+1=curr => close(prev,curr,M)) & (close(prev1,curr1,M) => prev1+1=curr1) ); var1 end; ex1 curr,prev,curr1,prev1,exdv1,exdv2 : ( validmodel(end,curr,prev,curr1,prev1,exdv1,exdv2) & minimalmodel(end,curr,prev,curr1,prev1,exdv1,exdv2) ) ;