:: deftheorem defines \Cup AOFA_L00:def 40 :
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 V3() 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 \Cup (P,K) = (Den ((In (( the connectives of S . (n + 7)), the carrier' of S)),L)) . <*P,K*>;