theorem Th73:
for
S being non
empty non
void bool-correct 11,1,1
-array 11
array-correct BoolSignature for
I being
integer SortSymbol of
S holds
(
the_array_sort_of S <> I & the
connectives of
S . 11
is_of_type <*(the_array_sort_of S),I*>,
I & the
connectives of
S . (11 + 1) is_of_type <*(the_array_sort_of S),I,I*>,
the_array_sort_of S & the
connectives of
S . (11 + 2) is_of_type <*(the_array_sort_of S)*>,
I & the
connectives of
S . (11 + 3) is_of_type <*I,I*>,
the_array_sort_of S )