:: deftheorem Def43 defines AL-closed AOFA_L00:def 47 :
for n being natural non empty number
for J being non empty non void Signature
for T being non-empty VarMSAlgebra over J
for X being non-empty 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 V being Formula of L
for F being Subset of ( the Sorts of L . the formula-sort of S) holds
( F is V AL-closed iff for A, B being Formula of L holds
( ( for M being Algorithm of L holds
( (M * (A \and B)) \iff ((M * A) \and (M * B)) in F & (M * (A \or B)) \iff ((M * A) \or (M * B)) in F & (\Cup (M,A)) \iff (A \or (\Cup (M,(M * A)))) in F & (\Cap (M,A)) \iff (A \and (\Cap (M,(M * A)))) in F & ( A \imp B in F implies ( (\Cup (M,A)) \imp (\Cup (M,B)) in F & (\Cap (M,A)) \imp (\Cap (M,B)) in F ) ) ) ) & ( for a being SortSymbol of J
for x being Element of X . a
for x0 being Element of Union (X extended_by ({}, the carrier of S)) st x = x0 holds
for t being Element of the Sorts of T . a
for t1 being Element of Union the Sorts of L st t1 = t holds
( ((x := (t,L)) * A) \iff (A / (x0,t1)) in F & ( for y being Element of X . a st y nin (vf t) . a holds
for y0 being Element of Union (X extended_by ({}, the carrier of S)) st y = y0 holds
((x := (t,L)) * (\ex (x,A))) \iff (\ex (y,((x := (t,L)) * ((y := ((@ x),L)) * (A / (x0,y0)))))) in F ) & ((x := (t,L)) * A) \imp (\ex (x,A)) in F ) ) & ( for M, M1, M2 being Algorithm of L holds
( ((M \; M1) * A) \iff (M * (M1 * A)) in F & ((if-then-else (M,M1,M2)) * A) \iff (((M * V) \and (M * (M1 * A))) \or ((M * (\not V)) \and (M * (M2 * A)))) in F & ((while (M,M1)) * A) \iff (((M * (\not V)) \and A) \or ((M * V) \and (M * (M1 * ((while (M,M1)) * A))))) in F ) ) ) );