let f be INT-Exec ; 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; for t being INT-Expression of NAT holds v,t form_assignment_wrt f
let t be INT-Expression of NAT; v,t form_assignment_wrt f
reconsider v9 = v as Element of Funcs ((Funcs (NAT,INT)),NAT) by FUNCT_2:8;
reconsider t9 = t as Element of Funcs ((Funcs (NAT,INT)),INT) by FUNCT_2:8;
A1:
Terminals (DTConUA (ECIW-signature,INT-ElemIns)) = INT-ElemIns
by FREEALG:3;
A2:
[v9,t9] in INT-ElemIns
by ZFMISC_1:87;
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
; AOFA_I00:def 15 ( 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; 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; verum