:: deftheorem Def26 defines valid_gcd_output NOMIN_4:def 26 :
for V, A being set
for z being Element of V
for x0, y0 being Nat
for b₆ being SCPartialNominativePredicate of V,A holds
( b₆ = valid_gcd_output (V,A,z,x0,y0) iff ( dom b₆ = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } & ( for d being object st d in dom b₆ holds
( ( valid_gcd_output_pred V,A,z,x0,y0,d implies b₆ . d = TRUE ) & ( not valid_gcd_output_pred V,A,z,x0,y0,d implies b₆ . d = FALSE ) ) ) ) );