:: deftheorem defines integer-array AOFA_A01:def 17 :
for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature
for X being non-empty ManySortedSet of the carrier of S
for T being non-empty b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for G being basic GeneratorSystem over S,X,T holds
( G is integer-array iff for I being integer SortSymbol of S holds
( { ((@ M) . t) where M is pure Element of the generators of G . (the_array_sort_of S), t is Element of T,I : verum } c= the generators of G . I & ( for M being pure Element of the generators of G . (the_array_sort_of S)
for t being Element of T,I
for g being Element of G,I st g = (@ M) . t holds
ex x being pure Element of the generators of G . I st
( x nin (vf t) . I & supp-var g = x & ((supp-term g) . (the_array_sort_of S)) . M = ((@ M),t) <- (@ x) & ( for s being SortSymbol of S
for y being pure Element of the generators of G . I st y in (vf g) . s & ( s = the_array_sort_of S implies y <> M ) holds
((supp-term g) . s) . y = y ) ) ) ) );