let f be INT-Exec ; :: thesis: for v being INT-Variable of NAT
for t being INT-Expression of NAT holds v,t form_assignment_wrt f
set S = ECIW-signature ;
set G = INT-ElemIns ;
set X = NAT ;
set A = FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ;
let v be INT-Variable of NAT ; :: thesis: for t being INT-Expression of NAT holds v,t form_assignment_wrt f
let t be INT-Expression of NAT ; :: thesis: v,t form_assignment_wrt f
reconsider v9 = v as Element of Funcs (Funcs NAT ,INT ),NAT by FUNCT_2:11;
reconsider t9 = t as Element of Funcs (Funcs NAT ,INT ),INT by FUNCT_2:11;
A1: Terminals (DTConUA ECIW-signature ,INT-ElemIns ) = INT-ElemIns by FREEALG:3;
A2: [v9,t9] in INT-ElemIns by ZFMISC_1:106;
A3: ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) = FreeGenSetNSG ECIW-signature ,INT-ElemIns by AOFA_000:70;
then root-tree [v9,t9] in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) by A1, A2;
then reconsider I = root-tree [v9,t9] as Element of (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) ;
take I ; :: according to AOFA_I00:def 15 :: thesis: ( I in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) & ( for s being Element of Funcs NAT ,INT holds f . s,I = s +* (v . s),(t . s) ) )
thus I in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) by A3, A1, A2; :: thesis: for s being Element of Funcs NAT ,INT holds f . s,I = s +* (v . s),(t . s)
thus for s being Element of Funcs NAT ,INT holds f . s,I = s +* (v . s),(t . s) by Def25; :: thesis: verum