let A be Euclidean preIfWhileAlgebra; :: thesis: for X being non empty countable set
for T being Subset of
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 v := t in ElementaryInstructions A
let X be non empty countable set ; :: thesis: for T being Subset of
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 v := t in ElementaryInstructions A
let T be Subset of ; :: 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 v := t in ElementaryInstructions A
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 v := t in ElementaryInstructions A
let v be INT-Variable of A,f; :: thesis: for t being INT-Expression of A,f holds v := t in ElementaryInstructions A
let t be INT-Expression of A,f; :: thesis: v := t in ElementaryInstructions A
set Y = { I where I is Element of : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } ;
v,t form_assignment_wrt f by Def22;
then consider I0 being Element of such that
A1: I0 in ElementaryInstructions A and
A2: for s being Element of Funcs X,INT holds f . s,I0 = s +* (v . s),(t . s) by Def15;
I0 in { I where I is Element of : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } by A1, A2;
then v := t in { I where I is Element of : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } ;
then ex I being Element of st
( v := t = I & I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) ;
hence v := t in ElementaryInstructions A ; :: thesis: verum