:: deftheorem Def17 defines -NorFunctor FOMODEL2:def 18 :
for S being Language
for U being non empty set
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN
for I being Element of U -InterpretersOf S
for phi being Element of ((AllSymbolsOf S) *) \ {{}} holds
( ( ex w1, w2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( [I,w1] in dom f & f . (I,w1) = FALSE & f . (I,w2) = FALSE & phi = (<*(TheNorSymbOf S)*> ^ w1) ^ w2 ) implies f -NorFunctor (I,phi) = TRUE ) & ( ( for w1, w2 being Element of ((AllSymbolsOf S) *) \ {{}} holds
( not [I,w1] in dom f or not f . (I,w1) = FALSE or not f . (I,w2) = FALSE or not phi = (<*(TheNorSymbOf S)*> ^ w1) ^ w2 ) ) implies f -NorFunctor (I,phi) = FALSE ) );