:: deftheorem Def24 defines valid_gcd_input NOMIN_4:def 24 :
for V, A being set
for x, y being object
for x0, y0 being Nat
for b₇ being SCPartialNominativePredicate of V,A holds
( b₇ = valid_gcd_input (V,A,x,y,x0,y0) iff ( dom b₇ = ND (V,A) & ( for d being object st d in dom b₇ holds
( ( valid_gcd_input_pred V,A,x,y,x0,y0,d implies b₇ . d = TRUE ) & ( not valid_gcd_input_pred V,A,x,y,x0,y0,d implies b₇ . d = FALSE ) ) ) ) );