let A be Euclidean preIfWhileAlgebra; :: thesis: for X being non empty countable set
for s being Element of Funcs X,INT
for T being Subset of (Funcs X,INT )
for f being Euclidean ExecutionFunction of A, Funcs X,INT ,T
for v being INT-Variable of A,f
for t being INT-Expression of A,f holds
( (f . s,(v := t)) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . s,(v := t)) . z = s . z ) )
let X be non empty countable set ; :: thesis: for s being Element of Funcs X,INT
for T being Subset of (Funcs X,INT )
for f being Euclidean ExecutionFunction of A, Funcs X,INT ,T
for v being INT-Variable of A,f
for t being INT-Expression of A,f holds
( (f . s,(v := t)) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . s,(v := t)) . z = s . z ) )
let s be Element of Funcs X,INT ; :: thesis: for T being Subset of (Funcs X,INT )
for f being Euclidean ExecutionFunction of A, Funcs X,INT ,T
for v being INT-Variable of A,f
for t being INT-Expression of A,f holds
( (f . s,(v := t)) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . s,(v := t)) . z = s . z ) )
let T be Subset of (Funcs X,INT ); :: thesis: for f being Euclidean ExecutionFunction of A, Funcs X,INT ,T
for v being INT-Variable of A,f
for t being INT-Expression of A,f holds
( (f . s,(v := t)) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . s,(v := t)) . z = s . z ) )
let f be Euclidean ExecutionFunction of A, Funcs X,INT ,T; :: thesis: for v being INT-Variable of A,f
for t being INT-Expression of A,f holds
( (f . s,(v := t)) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . s,(v := t)) . z = s . z ) )
let v be INT-Variable of A,f; :: thesis: for t being INT-Expression of A,f holds
( (f . s,(v := t)) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . s,(v := t)) . z = s . z ) )
let t be INT-Expression of A,f; :: thesis: ( (f . s,(v := t)) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . s,(v := t)) . z = s . z ) )
v,t form_assignment_wrt f by INT'iwa;
then consider I0 being Element of A such that
A0: I0 in ElementaryInstructions A and
A1: for s being Element of Funcs X,INT holds f . s,I0 = s +* (v . s),(t . s) by FA;
set Y = { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } ;
I0 in { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } by A0, A1;
then v := t in { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } ;
then consider I being Element of A such that
A2: v := t = I and
I in ElementaryInstructions A and
A3: for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ;
A4: f . s,(v := t) = s +* (v . s),(t . s) by A2, A3;
dom s = X by FUNCT_2:def 1;
hence ( (f . s,(v := t)) . (v . s) = t . s & ( for z being Element of X st z <> v . s holds
(f . s,(v := t)) . z = s . z ) ) by A4, FUNCT_7:33, FUNCT_7:34; :: thesis: verum