let S be non empty non void bool-correct 4,1 integer BoolSignature ; for X being V3() ManySortedSet of the carrier of S
for T being b1,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 V3() ManySortedSet of the carrier of S; 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; 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; 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; 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; 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; 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; 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); ( 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
; ( 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))
; 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; 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; 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; ( ((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
; ( ( 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 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;
( z <> x implies ((f . (s,(x := (t,A)))) . a) . z = (s . a) . z )assume A3:
z <> x
;
((f . (s,(x := (t,A)))) . a) . z = (s . a) . zA4:
(
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
;
verum
end;
let b be SortSymbol of S; ( 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
; for z being pure Element of the generators of G . b holds ((f . (s,(x := (t,A)))) . b) . z = (s . b) . z
hereby verum
let z be
pure Element of the
generators of
G . b;
((f . (s,(x := (t,A)))) . b) . z = (s . b) . zA7:
(
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
;
verum
end;