reconsider i0 = 0 as Element of INT by INT_1:def 1;
set Q = Funcs NAT ,INT ;
set T = (Funcs NAT ,INT ) \ 0 ,0 ;
reconsider b = 0 as Nat ;
set S = ECIW-signature ;
set G = INT-ElemIns ;
set A = FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ;
A1: Terminals (DTConUA ECIW-signature ,INT-ElemIns ) = INT-ElemIns by FREEALG:3;
reconsider q0 = NAT --> i0 as Element of Funcs NAT ,INT by FUNCT_2:11;
defpred S₁[ set , set ] means ex s being Element of Funcs NAT ,INT ex v being Element of Funcs (Funcs NAT ,INT ),NAT ex e being Element of Funcs (Funcs NAT ,INT ),INT st
( $1 = [s,(root-tree [v,e])] & $2 = s +* (v . s),(e . s) );
A2: ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) = FreeGenSetNSG ECIW-signature ,INT-ElemIns by AOFA_000:70;
A3: for x being set st x in [:(Funcs NAT ,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):] holds
ex y being set st
( y in Funcs NAT ,INT & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in [:(Funcs NAT ,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):] implies ex y being set st
( y in Funcs NAT ,INT & S₁[x,y] ) )
assume x in [:(Funcs NAT ,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):] ; :: thesis: ex y being set st
( y in Funcs NAT ,INT & S₁[x,y] )
then consider s, I being set such that
A4: s in Funcs NAT ,INT and
A5: I in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) and
A6: x = [s,I] by ZFMISC_1:def 2;
reconsider s = s as Element of Funcs NAT ,INT by A4;
consider a being Symbol of (DTConUA ECIW-signature ,INT-ElemIns ) such that
A7: I = root-tree a and
A8: a in Terminals (DTConUA ECIW-signature ,INT-ElemIns ) by A2, A5;
consider v, e being set such that
A9: v in Funcs (Funcs NAT ,INT ),NAT and
A10: e in Funcs (Funcs NAT ,INT ),INT and
A11: a = [v,e] by A1, A8, ZFMISC_1:def 2;
reconsider e = e as Element of Funcs (Funcs NAT ,INT ),INT by A10;
reconsider v = v as Element of Funcs (Funcs NAT ,INT ),NAT by A9;
take y = s +* (v . s),(e . s); :: thesis: ( y in Funcs NAT ,INT & S₁[x,y] )
thus y in Funcs NAT ,INT by FUNCT_2:11; :: thesis: S₁[x,y]
take s ; :: thesis: ex v being Element of Funcs (Funcs NAT ,INT ),NAT ex e being Element of Funcs (Funcs NAT ,INT ),INT st
( x = [s,(root-tree [v,e])] & y = s +* (v . s),(e . s) )
take v ; :: thesis: ex e being Element of Funcs (Funcs NAT ,INT ),INT st
( x = [s,(root-tree [v,e])] & y = s +* (v . s),(e . s) )
take e ; :: thesis: ( x = [s,(root-tree [v,e])] & y = s +* (v . s),(e . s) )
thus ( x = [s,(root-tree [v,e])] & y = s +* (v . s),(e . s) ) by A6, A7, A11; :: thesis: verum

end;

consider g being Function such that
A12: ( dom g = [:(Funcs NAT ,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):] & rng g c= Funcs NAT ,INT ) and
A13: for x being set st x in [:(Funcs NAT ,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):] holds
S₁[x,g . x] from WELLORD2:sch 1(A3);
reconsider g = g as Function of [:(Funcs NAT ,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):],(Funcs NAT ,INT ) by A12, FUNCT_2:4;
consider f being ExecutionFunction of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns , Funcs NAT ,INT ,(Funcs NAT ,INT ) \ 0 ,0 such that
A14: f | [:(Funcs NAT ,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):] = g and
for s being Element of Funcs NAT ,INT
for C, I being Element of (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) st not f iteration_terminates_for I \; C,f . s,C holds
f . s,(while C,I) = q0 by AOFA_000:91;
take f ; :: thesis: for s being Element of Funcs NAT ,INT
for v being Element of Funcs (Funcs NAT ,INT ),NAT
for e being Element of Funcs (Funcs NAT ,INT ),INT holds f . s,(root-tree [v,e]) = s +* (v . s),(e . s)
let s be Element of Funcs NAT ,INT ; :: thesis: for v being Element of Funcs (Funcs NAT ,INT ),NAT
for e being Element of Funcs (Funcs NAT ,INT ),INT holds f . s,(root-tree [v,e]) = s +* (v . s),(e . s)
let v be Element of Funcs (Funcs NAT ,INT ),NAT ; :: thesis: for e being Element of Funcs (Funcs NAT ,INT ),INT holds f . s,(root-tree [v,e]) = s +* (v . s),(e . s)
let e be Element of Funcs (Funcs NAT ,INT ),INT ; :: thesis: f . s,(root-tree [v,e]) = s +* (v . s),(e . s)
set I = root-tree [v,e];
[v,e] in INT-ElemIns by ZFMISC_1:106;
then root-tree [v,e] in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) by A2, A1;
then A15: [s,(root-tree [v,e])] in [:(Funcs NAT ,INT ),(ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns )):] by ZFMISC_1:106;
then consider s9 being Element of Funcs NAT ,INT , v9 being Element of Funcs (Funcs NAT ,INT ),NAT , e9 being Element of Funcs (Funcs NAT ,INT ),INT such that
A16: [s,(root-tree [v,e])] = [s9,(root-tree [v9,e9])] and
A17: g . [s,(root-tree [v,e])] = s9 +* (v9 . s9),(e9 . s9) by A13;
root-tree [v,e] = root-tree [v9,e9] by A16, ZFMISC_1:33;
then A18: [v,e] = [v9,e9] by TREES_4:4;
then A19: v = v9 by ZFMISC_1:33;
A20: e = e9 by A18, ZFMISC_1:33;
s = s9 by A16, ZFMISC_1:33;
hence f . s,(root-tree [v,e]) = s +* (v . s),(e . s) by A14, A15, A17, A19, A20, FUNCT_1:72; :: thesis: verum