let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G st A is elementary holds
for a being SortSymbol of S
for x being Element of the generators of G . a
for t being Element of T,a holds x := (t,A) in ElementaryInstructions A
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G st A is elementary holds
for a being SortSymbol of S
for x being Element of the generators of G . a
for t being Element of T,a holds x := (t,A) in ElementaryInstructions A
let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S; :: thesis: for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G st A is elementary holds
for a being SortSymbol of S
for x being Element of the generators of G . a
for t being Element of T,a holds x := (t,A) in ElementaryInstructions A
let G be basic GeneratorSystem over S,X,T; :: thesis: for A being IfWhileAlgebra of the generators of G st A is elementary holds
for a being SortSymbol of S
for x being Element of the generators of G . a
for t being Element of T,a holds x := (t,A) in ElementaryInstructions A
let A be IfWhileAlgebra of the generators of G; :: thesis: ( A is elementary implies for a being SortSymbol of S
for x being Element of the generators of G . a
for t being Element of T,a holds x := (t,A) in ElementaryInstructions A )
assume A1: rng the assignments of A c= ElementaryInstructions A ; :: according to AOFA_A01:def 13 :: thesis: for a being SortSymbol of S
for x being Element of the generators of G . a
for t being Element of T,a holds x := (t,A) in ElementaryInstructions A
let a be SortSymbol of S; :: thesis: for x being Element of the generators of G . a
for t being Element of T,a holds x := (t,A) in ElementaryInstructions A
let x be Element of the generators of G . a; :: thesis: for t being Element of T,a holds x := (t,A) in ElementaryInstructions A
let t be Element of T,a; :: thesis: x := (t,A) in ElementaryInstructions A
[x,t] in [:( the generators of G . a),( the Sorts of T . a):] by ZFMISC_1:87;
then ( [x,t] in [| the generators of G, the Sorts of T|] . a & dom [| the generators of G, the Sorts of T|] = the carrier of S ) by PARTFUN1:def 2, PBOOLE:def 16;
then x := (t,A) in rng the assignments of A by FUNCT_2:4, CARD_5:2;
hence x := (t,A) in ElementaryInstructions A by A1; :: thesis: verum