:: deftheorem Def18 defines NorIterator FOMODEL2:def 19 :
for S being Language
for U being non empty set
for g being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)
for b₄ being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN holds
( b₄ = NorIterator g iff ( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b₄ iff ex phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [x,phi1] in dom g & [x,phi2] in dom g ) ) ) & ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b₄ holds
b₄ . (x,y) = g -NorFunctor (x,y) ) ) );