:: deftheorem Def35 defines TerminatingPrograms AOFA_000:def 35 :
for A being preIfWhileAlgebra
for S being non empty set
for T being Subset of S
for f being ExecutionFunction of A,S,T
for b₅ being Subset of [:S, the carrier of A:] holds
( b₅ = TerminatingPrograms (A,S,T,f) iff ( [:S,(ElementaryInstructions A):] c= b₅ & [:S,{(EmptyIns A)}:] c= b₅ & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in b₅ & [(f . (s,I)),J] in b₅ implies [s,(I \; J)] in b₅ ) & ( [s,C] in b₅ & [(f . (s,C)),I] in b₅ & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in b₅ ) & ( [s,C] in b₅ & [(f . (s,C)),J] in b₅ & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in b₅ ) & ( [s,C] in b₅ & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in b₅ & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in b₅ ) ) ) & ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds
b₅ c= P ) ) );