theorem Th67: :: AOFA_A01:67

for S being non empty non void bool-correct 4,1 integer BoolSignature
for X being non-empty ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G
for I being integer SortSymbol of S
for b being pure Element of the generators of G . the bool-sort of S
for t being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )