:: deftheorem defines array-degenerated AOFA_A01:def 20 :
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 b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds
( T is array-degenerated iff ex I being integer SortSymbol of S ex M being Element of (FreeGen T) . (the_array_sort_of S) ex t being Element of T,I st (@ M) . t <> (Sym ((In (( the connectives of S . 11), the carrier' of S)),X)) -tree <*M,t*> );