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 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 b being pure Element of the generators of G . the bool-sort of S
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
for a being SortSymbol of S
for x being pure Element of the generators of G . a
for t being Element of T,a holds
( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )
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 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 b being pure Element of the generators of G . the bool-sort of S
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
for a being SortSymbol of S
for x being pure Element of the generators of G . a
for t being Element of T,a holds
( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )
let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S; :: thesis: 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 b being pure Element of the generators of G . the bool-sort of S
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
for a being SortSymbol of S
for x being pure Element of the generators of G . a
for t being Element of T,a holds
( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )
let C be bool-correct 4,1 integer image of T; :: thesis: for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G
for b being pure Element of the generators of G . the bool-sort of S
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
for a being SortSymbol of S
for x being pure Element of the generators of G . a
for t being Element of T,a holds
( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )
let G be basic GeneratorSystem over S,X,T; :: thesis: for A being IfWhileAlgebra of the generators of G
for b being pure Element of the generators of G . the bool-sort of S
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
for a being SortSymbol of S
for x being pure Element of the generators of G . a
for t being Element of T,a holds
( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )
let A be IfWhileAlgebra of the generators of G; :: thesis: for b being pure Element of the generators of G . the bool-sort of S
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
for a being SortSymbol of S
for x being pure Element of the generators of G . a
for t being Element of T,a holds
( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )
let b be pure Element of the generators of G . the bool-sort of S; :: thesis: 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
for a being SortSymbol of S
for x being pure Element of the generators of G . a
for t being Element of T,a holds
( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )
let s be Element of C -States the generators of G; :: thesis: 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
for a being SortSymbol of S
for x being pure Element of the generators of G . a
for t being Element of T,a holds
( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )
let f be ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b); :: thesis: ( G is C -supported & f in C -Execution (A,b,(\false C)) implies for a being SortSymbol of S
for x being pure Element of the generators of G . a
for t being Element of T,a holds
( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) ) )
assume A1: G is C -supported ; :: thesis: ( not f in C -Execution (A,b,(\false C)) or for a being SortSymbol of S
for x being pure Element of the generators of G . a
for t being Element of T,a holds
( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) ) )
assume A2: f in C -Execution (A,b,(\false C)) ; :: thesis: for a being SortSymbol of S
for x being pure Element of the generators of G . a
for t being Element of T,a holds
( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )
let a be SortSymbol of S; :: thesis: for x being pure Element of the generators of G . a
for t being Element of T,a holds
( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )
let x be pure Element of the generators of G . a; :: thesis: for t being Element of T,a holds
( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )
let t be Element of T,a; :: thesis: ( ((f . (s,(x := (t,A)))) . a) . x = t value_at (C,s) & ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )
reconsider x0 = @ x as Element of G,a by AOFA_A00:def 22;
thus ((f . (s,(x := (t,A)))) . a) . x = ((succ (s,x0,(t value_at (C,s)))) . a) . x by A2, AOFA_A00:def 28
.= t value_at (C,s) by A1, AOFA_A00:def 27 ; :: thesis: ( ( for z being pure Element of the generators of G . a st z <> x holds
((f . (s,(x := (t,A)))) . a) . z = (s . a) . z ) & ( for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z ) )

hereby :: thesis: for b being SortSymbol of S st a <> b holds
for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z

let z be pure Element of the generators of G . a; :: thesis: ( z <> x implies ((f . (s,(x := (t,A)))) . a) . z = (s . a) . z )
assume A3: z <> x ; :: thesis: ((f . (s,(x := (t,A)))) . a) . z = (s . a) . z
A4: ( x in (FreeGen T) . a & z in (FreeGen T) . a & FreeGen X is ManySortedSubset of the generators of G ) by A1, Def4;
then ( vf (@ x) = a -singleton x & FreeGen X c= the generators of G ) by AOFA_A00:41, PBOOLE:def 18;
then ( (vf (@ x)) . a = {x} & (FreeGen X) . a c= the generators of G . a ) by AOFA_A00:6;
then A5: ( z nin (vf (@ x)) . a & @ x is Element of G,a ) by A3, TARSKI:def 1, AOFA_A00:def 22;
thus ((f . (s,(x := (t,A)))) . a) . z = ((succ (s,x0,(t value_at (C,s)))) . a) . z by A2, AOFA_A00:def 28
.= (s . a) . z by A1, A3, A5, A4, AOFA_A00:def 27 ; :: thesis: verum

end;

let b be SortSymbol of S; :: thesis: ( a <> b implies for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z )
assume A6: a <> b ; :: thesis: for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z

hereby :: thesis: verum

let z be pure Element of the generators of G . b; :: thesis: ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z
A7: ( x in (FreeGen T) . a & z in (FreeGen T) . b & FreeGen X is ManySortedSubset of the generators of G ) by A1, Def4;
then ( vf (@ x) = a -singleton x & FreeGen X c= the generators of G ) by AOFA_A00:41, PBOOLE:def 18;
then A8: ( z nin (vf (@ x)) . b & @ x is Element of G,a ) by A6, AOFA_A00:6, AOFA_A00:def 22;
thus ((f . (s,(x := (t,A)))) . b) . z = ((succ (s,x0,(t value_at (C,s)))) . b) . z by A2, AOFA_A00:def 28
.= (s . b) . z by A1, A6, A8, A7, AOFA_A00:def 27 ; :: thesis: verum

end;