:: deftheorem Def6 defines AL-correct AOFA_L00:def 6 :
for n being Nat
for X being set
for L being AlgLangSignature over X holds
( L is n AL-correct iff ( the program-sort of L <> the formula-sort of L & len the connectives of L >= n + 8 & the connectives of L . (n + 6) is_of_type <* the program-sort of L, the formula-sort of L*>, the formula-sort of L & ... & the connectives of L . (n + 8) is_of_type <* the program-sort of L, the formula-sort of L*>, the formula-sort of L ) );