:: deftheorem defines * AOFA_L00:def 39 :
for n being non empty Nat
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being empty-yielding GeneratorSet of T
for S being non empty non void b₂ -extension b₁ PC-correct QC-correct b₁ AL-correct essential AlgLangSignature over Union X
for L being IfWhileAlgebra of X,S
for K being Formula of L
for P being Algorithm of L holds P * K = (Den ((In (( the connectives of S . (n + 6)), the carrier' of S)),L)) . <*P,K*>;